Loogle!

Result

Found 116 declarations mentioning Finset.HasAntidiagonal.antidiagonal.

Finset.HasAntidiagonal.antidiagonal 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} {inst✝ : AddMonoid A} [self : Finset.HasAntidiagonal A] : A → Finset (A × A)
Finset.hasAntidiagonal_congr 📋 Mathlib.Algebra.Order.Antidiag.Prod
(A : Type u_2) [AddMonoid A] [H1 : Finset.HasAntidiagonal A] [H2 : Finset.HasAntidiagonal A] : Finset.antidiagonal = Finset.antidiagonal
Finset.map_prodComm_antidiagonal 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] {n : A} : Finset.map (Equiv.prodComm A A).toEmbedding (Finset.antidiagonal n) = Finset.antidiagonal n
Finset.sigmaAntidiagonalEquivProd 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddMonoid A] [Finset.HasAntidiagonal A] : (n : A) × ↥(Finset.antidiagonal n) ≃ A × A
Finset.map_swap_antidiagonal 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] {n : A} : Finset.map { toFun := Prod.swap, inj' := ⋯ } (Finset.antidiagonal n) = Finset.antidiagonal n
Finset.HasAntidiagonal.mem_antidiagonal 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} {inst✝ : AddMonoid A} [self : Finset.HasAntidiagonal A] {n : A} {a : A × A} : a ∈ Finset.antidiagonal n ↔ a.1 + a.2 = n
Finset.swap_mem_antidiagonal 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] {n : A} {xy : A × A} : xy.swap ∈ Finset.antidiagonal n ↔ xy ∈ Finset.antidiagonal n
Finset.antidiagonal.fst_le 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Finset.HasAntidiagonal A] {n : A} {kl : A × A} (hlk : kl ∈ Finset.antidiagonal n) : kl.1 ≤ n
Finset.antidiagonal.snd_le 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Finset.HasAntidiagonal A] {n : A} {kl : A × A} (hlk : kl ∈ Finset.antidiagonal n) : kl.2 ≤ n
Finset.antidiagonal_congr 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCancelMonoid A] [Finset.HasAntidiagonal A] {p q : A × A} {n : A} (hp : p ∈ Finset.antidiagonal n) (hq : q ∈ Finset.antidiagonal n) : p = q ↔ p.1 = q.1
Finset.antidiagonal_congr' 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCancelCommMonoid A] [Finset.HasAntidiagonal A] {p q : A × A} {n : A} (hp : p ∈ Finset.antidiagonal n) (hq : q ∈ Finset.antidiagonal n) : p = q ↔ p.2 = q.2
Finset.antidiagonal_zero 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Finset.HasAntidiagonal A] : Finset.antidiagonal 0 = {(0, 0)}
Finset.filter_fst_eq_antidiagonal 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Sub A] [OrderedSub A] [AddLeftReflectLE A] [Finset.HasAntidiagonal A] (n m : A) [DecidablePred fun x => x = m] [Decidable (m ≤ n)] : {x ∈ Finset.antidiagonal n | x.1 = m} = if m ≤ n then {(m, n - m)} else ∅
Finset.filter_snd_eq_antidiagonal 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Sub A] [OrderedSub A] [AddLeftReflectLE A] [Finset.HasAntidiagonal A] (n m : A) [DecidablePred fun x => x = m] [Decidable (m ≤ n)] : {x ∈ Finset.antidiagonal n | x.2 = m} = if m ≤ n then {(n - m, m)} else ∅
Finset.antidiagonal_subtype_ext 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCancelMonoid A] [Finset.HasAntidiagonal A] {n : A} {p q : ↥(Finset.antidiagonal n)} (h : (↑p).1 = (↑q).1) : p = q
Finset.antidiagonal_subtype_ext_iff 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCancelMonoid A] [Finset.HasAntidiagonal A] {n : A} {p q : ↥(Finset.antidiagonal n)} : p = q ↔ (↑p).1 = (↑q).1
Finset.sigmaAntidiagonalEquivProd_symm_apply_fst 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddMonoid A] [Finset.HasAntidiagonal A] (x : A × A) : (Finset.sigmaAntidiagonalEquivProd.symm x).fst = x.1 + x.2
Finset.sigmaAntidiagonalEquivProd_symm_apply_snd_coe 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddMonoid A] [Finset.HasAntidiagonal A] (x : A × A) : ↑(Finset.sigmaAntidiagonalEquivProd.symm x).snd = x
Finset.sigmaAntidiagonalEquivProd_apply 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddMonoid A] [Finset.HasAntidiagonal A] (x : (n : A) × ↥(Finset.antidiagonal n)) : Finset.sigmaAntidiagonalEquivProd x = ↑x.snd
Finset.Nat.card_antidiagonal 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) : (Finset.antidiagonal n).card = n + 1
Finset.Nat.antidiagonal_zero 📋 Mathlib.Data.Finset.NatAntidiagonal
: Finset.antidiagonal 0 = {(0, 0)}
Finset.Nat.antidiagonal.fst_lt 📋 Mathlib.Data.Finset.NatAntidiagonal
{n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ Finset.antidiagonal n) : kl.1 < n + 1
Finset.Nat.antidiagonal.snd_lt 📋 Mathlib.Data.Finset.NatAntidiagonal
{n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ Finset.antidiagonal n) : kl.2 < n + 1
Finset.Nat.antidiagonalEquivFin 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) : ↥(Finset.antidiagonal n) ≃ Fin (n + 1)
Finset.Nat.antidiagonal_eq_image 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) : Finset.antidiagonal n = Finset.image (fun i => (i, n - i)) (Finset.range (n + 1))
Finset.Nat.antidiagonal_eq_image' 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) : Finset.antidiagonal n = Finset.image (fun i => (n - i, i)) (Finset.range (n + 1))
Finset.Nat.antidiagonal_succ 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) : Finset.antidiagonal (n + 1) = Finset.cons (0, n + 1) (Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) (Finset.antidiagonal n)) ⋯
Finset.Nat.antidiagonal_succ' 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) : Finset.antidiagonal (n + 1) = Finset.cons (n + 1, 0) (Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (Finset.antidiagonal n)) ⋯
Finset.Nat.antidiagonal_filter_le_fst_of_le 📋 Mathlib.Data.Finset.NatAntidiagonal
{n k : ℕ} (h : k ≤ n) : {a ∈ Finset.antidiagonal n | k ≤ a.1} = Finset.map ({ toFun := fun x => x + k, inj' := ⋯ }.prodMap (Function.Embedding.refl ℕ)) (Finset.antidiagonal (n - k))
Finset.Nat.antidiagonal_filter_le_snd_of_le 📋 Mathlib.Data.Finset.NatAntidiagonal
{n k : ℕ} (h : k ≤ n) : {a ∈ Finset.antidiagonal n | k ≤ a.2} = Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (Finset.antidiagonal (n - k))
Finset.Nat.antidiagonal_filter_fst_le_of_le 📋 Mathlib.Data.Finset.NatAntidiagonal
{n k : ℕ} (h : k ≤ n) : {a ∈ Finset.antidiagonal n | a.1 ≤ k} = Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := fun x => x + (n - k), inj' := ⋯ }) (Finset.antidiagonal k)
Finset.Nat.antidiagonal_filter_snd_le_of_le 📋 Mathlib.Data.Finset.NatAntidiagonal
{n k : ℕ} (h : k ≤ n) : {a ∈ Finset.antidiagonal n | a.2 ≤ k} = Finset.map ({ toFun := fun x => x + (n - k), inj' := ⋯ }.prodMap (Function.Embedding.refl ℕ)) (Finset.antidiagonal k)
Finset.Nat.antidiagonal_succ_succ' 📋 Mathlib.Data.Finset.NatAntidiagonal
{n : ℕ} : Finset.antidiagonal (n + 2) = Finset.cons (0, n + 2) (Finset.cons (n + 2, 0) (Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (Finset.antidiagonal n)) ⋯) ⋯
Finset.Nat.antidiagonal_eq_map 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) : Finset.antidiagonal n = Finset.map { toFun := fun i => (i, n - i), inj' := ⋯ } (Finset.range (n + 1))
Finset.Nat.antidiagonal_eq_map' 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) : Finset.antidiagonal n = Finset.map { toFun := fun i => (n - i, i), inj' := ⋯ } (Finset.range (n + 1))
Finset.Nat.antidiagonalEquivFin_apply_val 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) (x✝ : ↥(Finset.antidiagonal n)) : ↑((Finset.Nat.antidiagonalEquivFin n) x✝) = x✝.1.1
Finset.Nat.antidiagonalEquivFin_symm_apply_coe 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) (x✝ : Fin (n + 1)) : ↑((Finset.Nat.antidiagonalEquivFin n).symm x✝) = (↑x✝, n - ↑x✝)
Finset.Nat.prod_antidiagonal_swap 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_1} [CommMonoid M] {n : ℕ} {f : ℕ × ℕ → M} : ∏ p ∈ Finset.antidiagonal n, f p.swap = ∏ p ∈ Finset.antidiagonal n, f p
Finset.Nat.sum_antidiagonal_swap 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_1} [AddCommMonoid M] {n : ℕ} {f : ℕ × ℕ → M} : ∑ p ∈ Finset.antidiagonal n, f p.swap = ∑ p ∈ Finset.antidiagonal n, f p
Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_3} [CommMonoid M] (f : ℕ × ℕ → M) (n : ℕ) : ∏ ij ∈ Finset.antidiagonal n, f ij = ∏ k ∈ Finset.range n.succ, f (k, n - k)
Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_3} [AddCommMonoid M] (f : ℕ × ℕ → M) (n : ℕ) : ∑ ij ∈ Finset.antidiagonal n, f ij = ∑ k ∈ Finset.range n.succ, f (k, n - k)
Finset.Nat.prod_antidiagonal_eq_prod_range_succ 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_3} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ∏ ij ∈ Finset.antidiagonal n, f ij.1 ij.2 = ∏ k ∈ Finset.range n.succ, f k (n - k)
Finset.Nat.sum_antidiagonal_eq_sum_range_succ 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_3} [AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ∑ ij ∈ Finset.antidiagonal n, f ij.1 ij.2 = ∑ k ∈ Finset.range n.succ, f k (n - k)
Finset.Nat.prod_antidiagonal_subst 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_1} [CommMonoid M] {n : ℕ} {f : ℕ × ℕ → ℕ → M} : ∏ p ∈ Finset.antidiagonal n, f p n = ∏ p ∈ Finset.antidiagonal n, f p (p.1 + p.2)
Finset.Nat.sum_antidiagonal_subst 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_1} [AddCommMonoid M] {n : ℕ} {f : ℕ × ℕ → ℕ → M} : ∑ p ∈ Finset.antidiagonal n, f p n = ∑ p ∈ Finset.antidiagonal n, f p (p.1 + p.2)
Finset.Nat.sum_antidiagonal_succ 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{N : Type u_2} [AddCommMonoid N] {n : ℕ} {f : ℕ × ℕ → N} : ∑ p ∈ Finset.antidiagonal (n + 1), f p = f (0, n + 1) + ∑ p ∈ Finset.antidiagonal n, f (p.1 + 1, p.2)
Finset.Nat.sum_antidiagonal_succ' 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{N : Type u_2} [AddCommMonoid N] {n : ℕ} {f : ℕ × ℕ → N} : ∑ p ∈ Finset.antidiagonal (n + 1), f p = f (n + 1, 0) + ∑ p ∈ Finset.antidiagonal n, f (p.1, p.2 + 1)
Finset.Nat.prod_antidiagonal_succ 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_1} [CommMonoid M] {n : ℕ} {f : ℕ × ℕ → M} : ∏ p ∈ Finset.antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p ∈ Finset.antidiagonal n, f (p.1 + 1, p.2)
Finset.Nat.prod_antidiagonal_succ' 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_1} [CommMonoid M] {n : ℕ} {f : ℕ × ℕ → M} : ∏ p ∈ Finset.antidiagonal (n + 1), f p = f (n + 1, 0) * ∏ p ∈ Finset.antidiagonal n, f (p.1, p.2 + 1)
Finset.sum_antidiagonal_choose_add 📋 Mathlib.Data.Nat.Choose.Sum
(d n : ℕ) : ∑ ij ∈ Finset.antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
Commute.add_pow' 📋 Mathlib.Data.Nat.Choose.Sum
{R : Type u_1} [Semiring R] {x y : R} (h : Commute x y) (n : ℕ) : (x + y) ^ n = ∑ m ∈ Finset.antidiagonal n, n.choose m.1 • (x ^ m.1 * y ^ m.2)
Finset.prod_antidiagonal_pow_choose_succ 📋 Mathlib.Data.Nat.Choose.Sum
{M : Type u_2} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ∏ ij ∈ Finset.antidiagonal (n + 1), f ij.1 ij.2 ^ (n + 1).choose ij.1 = (∏ ij ∈ Finset.antidiagonal n, f ij.1 (ij.2 + 1) ^ n.choose ij.1) * ∏ ij ∈ Finset.antidiagonal n, f (ij.1 + 1) ij.2 ^ n.choose ij.2
Finset.sum_antidiagonal_choose_succ_nsmul 📋 Mathlib.Data.Nat.Choose.Sum
{M : Type u_2} [AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ∑ ij ∈ Finset.antidiagonal (n + 1), (n + 1).choose ij.1 • f ij.1 ij.2 = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • f ij.1 (ij.2 + 1) + ∑ ij ∈ Finset.antidiagonal n, n.choose ij.2 • f (ij.1 + 1) ij.2
Finset.sum_antidiagonal_choose_succ_mul 📋 Mathlib.Data.Nat.Choose.Sum
{R : Type u_1} [NonAssocSemiring R] (f : ℕ → ℕ → R) (n : ℕ) : ∑ ij ∈ Finset.antidiagonal (n + 1), ↑((n + 1).choose ij.1) * f ij.1 ij.2 = ∑ ij ∈ Finset.antidiagonal n, ↑(n.choose ij.1) * f ij.1 (ij.2 + 1) + ∑ ij ∈ Finset.antidiagonal n, ↑(n.choose ij.2) * f (ij.1 + 1) ij.2
Polynomial.coeff_mul 📋 Mathlib.Algebra.Polynomial.Coeff
{R : Type u} [Semiring R] (p q : Polynomial R) (n : ℕ) : (p * q).coeff n = ∑ x ∈ Finset.antidiagonal n, p.coeff x.1 * q.coeff x.2
Finsupp.antidiagonal_single 📋 Mathlib.Data.Finsupp.Antidiagonal
{α : Type u} [DecidableEq α] (a : α) (n : ℕ) : (Finset.antidiagonal fun₀ | a => n) = Finset.map ({ toFun := Finsupp.single a, inj' := ⋯ }.prodMap { toFun := Finsupp.single a, inj' := ⋯ }) (Finset.antidiagonal n)
Finsupp.antidiagonal_zero 📋 Mathlib.Data.Finsupp.Antidiagonal
{α : Type u} [DecidableEq α] : Finset.antidiagonal 0 = {(0, 0)}
Finsupp.prod_antidiagonal_swap 📋 Mathlib.Data.Finsupp.Antidiagonal
{α : Type u} [DecidableEq α] {M : Type u_1} [CommMonoid M] (n : α →₀ ℕ) (f : (α →₀ ℕ) → (α →₀ ℕ) → M) : ∏ p ∈ Finset.antidiagonal n, f p.1 p.2 = ∏ p ∈ Finset.antidiagonal n, f p.2 p.1
Finsupp.sum_antidiagonal_swap 📋 Mathlib.Data.Finsupp.Antidiagonal
{α : Type u} [DecidableEq α] {M : Type u_1} [AddCommMonoid M] (n : α →₀ ℕ) (f : (α →₀ ℕ) → (α →₀ ℕ) → M) : ∑ p ∈ Finset.antidiagonal n, f p.1 p.2 = ∑ p ∈ Finset.antidiagonal n, f p.2 p.1
MvPolynomial.coeff_mul 📋 Mathlib.Algebra.MvPolynomial.Basic
{R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p q : MvPolynomial σ R) (n : σ →₀ ℕ) : MvPolynomial.coeff n (p * q) = ∑ x ∈ Finset.antidiagonal n, MvPolynomial.coeff x.1 p * MvPolynomial.coeff x.2 q
summable_sum_mul_antidiagonal_of_summable_mul 📋 Mathlib.Topology.Algebra.InfiniteSum.Ring
{α : Type u_3} {A : Type u_4} [AddCommMonoid A] [Finset.HasAntidiagonal A] [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : A → α} [T3Space α] [IsTopologicalSemiring α] (h : Summable fun x => f x.1 * g x.2) : Summable fun n => ∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2
Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal 📋 Mathlib.Topology.Algebra.InfiniteSum.Ring
{α : Type u_3} {A : Type u_4} [AddCommMonoid A] [Finset.HasAntidiagonal A] [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : A → α} [T3Space α] [IsTopologicalSemiring α] (hf : Summable f) (hg : Summable g) (hfg : Summable fun x => f x.1 * g x.2) : (∑' (n : A), f n) * ∑' (n : A), g n = ∑' (n : A), ∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2
summable_mul_prod_iff_summable_mul_sigma_antidiagonal 📋 Mathlib.Topology.Algebra.InfiniteSum.Ring
{α : Type u_3} {A : Type u_4} [AddCommMonoid A] [Finset.HasAntidiagonal A] [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : A → α} : (Summable fun x => f x.1 * g x.2) ↔ Summable fun x => f (↑x.snd).1 * g (↑x.snd).2
Finset.Nat.antidiagonalTuple_two 📋 Mathlib.Data.Fin.Tuple.NatAntidiagonal
(n : ℕ) : Finset.Nat.antidiagonalTuple 2 n = Finset.map (piFinTwoEquiv fun x => ℕ).symm.toEmbedding (Finset.antidiagonal n)
Finset.finsetCongr_piAntidiag_eq_antidiag 📋 Mathlib.Algebra.Order.Antidiag.Pi
{μ : Type u_2} [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] (n : μ) : (Equiv.boolArrowEquivProd μ).finsetCongr (Finset.univ.piAntidiag n) = Finset.antidiagonal n
Finset.piAntidiag_insert 📋 Mathlib.Algebra.Order.Antidiag.Pi
{ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCancelCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] {i : ι} {s : Finset ι} [DecidableEq (ι → μ)] (hi : i ∉ s) (n : μ) : (insert i s).piAntidiag n = (Finset.antidiagonal n).biUnion fun p => Finset.image (fun f j => f j + if j = i then p.1 else 0) (s.piAntidiag p.2)
Finset.pairwiseDisjoint_piAntidiag_map_addRightEmbedding 📋 Mathlib.Algebra.Order.Antidiag.Pi
{ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCancelCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] {i : ι} {s : Finset ι} (hi : i ∉ s) (n : μ) : (↑(Finset.antidiagonal n)).PairwiseDisjoint fun p => Finset.map (addRightEmbedding fun j => if j = i then p.1 else 0) (s.piAntidiag p.2)
Finset.piAntidiag_cons 📋 Mathlib.Algebra.Order.Antidiag.Pi
{ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCancelCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] {i : ι} {s : Finset ι} (hi : i ∉ s) (n : μ) : (Finset.cons i s hi).piAntidiag n = (Finset.antidiagonal n).disjiUnion (fun p => Finset.map (addRightEmbedding fun t => if t = i then p.1 else 0) (s.piAntidiag p.2)) ⋯
Finset.mem_finsuppAntidiag_insert 📋 Mathlib.Algebra.Order.Antidiag.Finsupp
{ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] {a : ι} {s : Finset ι} (h : a ∉ s) (n : μ) {f : ι →₀ μ} : f ∈ (insert a s).finsuppAntidiag n ↔ ∃ m ∈ Finset.antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2
Finset.finsuppAntidiag_insert 📋 Mathlib.Algebra.Order.Antidiag.Finsupp
{ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] {a : ι} {s : Finset ι} (h : a ∉ s) (n : μ) : (insert a s).finsuppAntidiag n = (Finset.antidiagonal n).biUnion fun p => Finset.map { toFun := fun f => (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach
PolynomialModule.smul_apply 📋 Mathlib.Algebra.Polynomial.Module.Basic
{R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (f : Polynomial R) (g : PolynomialModule R M) (n : ℕ) : (f • g) n = ∑ x ∈ Finset.antidiagonal n, f.coeff x.1 • g x.2
DirectSum.coe_mul_apply_eq_sum_antidiagonal 📋 Mathlib.Algebra.DirectSum.Internal
{ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddMonoid ι] [Finset.HasAntidiagonal ι] [SetLike.GradedMonoid A] (r r' : DirectSum ι fun i => ↥(A i)) (n : ι) : ↑((r * r') n) = ∑ ij ∈ Finset.antidiagonal n, ↑(r ij.1) * ↑(r' ij.2)
PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_2 📋 Mathlib.RingTheory.PolynomialAlgebra
(R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (k : ℕ) (a₁ a₂ : A) (p₁ p₂ : Polynomial R) : a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) = ∑ x ∈ Finset.antidiagonal k, a₁ * (algebraMap R A) (p₁.coeff x.1) * (a₂ * (algebraMap R A) (p₂.coeff x.2))
Nat.add_choose_eq 📋 Mathlib.Data.Nat.Choose.Vandermonde
(m n k : ℕ) : (m + n).choose k = ∑ ij ∈ Finset.antidiagonal k, m.choose ij.1 * n.choose ij.2
Polynomial.hasseDeriv_mul 📋 Mathlib.Algebra.Polynomial.HasseDeriv
{R : Type u_1} [Semiring R] (k : ℕ) (f g : Polynomial R) : (Polynomial.hasseDeriv k) (f * g) = ∑ ij ∈ Finset.antidiagonal k, (Polynomial.hasseDeriv ij.1) f * (Polynomial.hasseDeriv ij.2) g
Nat.fib_succ_eq_sum_choose 📋 Mathlib.Data.Nat.Fib.Basic
(n : ℕ) : Nat.fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2
LieModule.toEnd_pow_lie 📋 Mathlib.Algebra.Lie.OfAssociative
(R : Type u) {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x y : L) (z : M) (n : ℕ) : ((LieModule.toEnd R L M) x ^ n) ⁅y, z⁆ = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • ⁅((LieAlgebra.ad R L) x ^ ij.1) y, ((LieModule.toEnd R L M) x ^ ij.2) z⁆
LieAlgebra.ad_pow_lie 📋 Mathlib.Algebra.Lie.OfAssociative
(R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x y z : L) (n : ℕ) : ((LieAlgebra.ad R L) x ^ n) ⁅y, z⁆ = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • ⁅((LieAlgebra.ad R L) x ^ ij.1) y, ((LieAlgebra.ad R L) x ^ ij.2) z⁆
LieDerivation.iterate_apply_lie 📋 Mathlib.Algebra.Lie.Derivation.Basic
{R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (n : ℕ) (a b : L) : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
summable_norm_sum_mul_antidiagonal_of_summable_norm 📋 Mathlib.Analysis.Normed.Ring.InfiniteSum
{R : Type u_1} [NormedRing R] {f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) : Summable fun n => ‖∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2‖
summable_sum_mul_antidiagonal_of_summable_norm' 📋 Mathlib.Analysis.Normed.Ring.InfiniteSum
{R : Type u_1} [NormedRing R] {f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (h'f : Summable f) (hg : Summable fun x => ‖g x‖) (h'g : Summable g) : Summable fun n => ∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2
tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm 📋 Mathlib.Analysis.Normed.Ring.InfiniteSum
{R : Type u_1} [NormedRing R] [CompleteSpace R] {f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) : (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2
tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm' 📋 Mathlib.Analysis.Normed.Ring.InfiniteSum
{R : Type u_1} [NormedRing R] {f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (h'f : Summable f) (hg : Summable fun x => ‖g x‖) (h'g : Summable g) : (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2
Polynomial.homogenize.eq_1 📋 Mathlib.Algebra.Polynomial.Homogenize
{R : Type u_1} [CommSemiring R] (p : Polynomial R) (n : ℕ) : p.homogenize n = ∑ kl ∈ Finset.antidiagonal n, (MvPolynomial.monomial fun₀ | 0 => kl.1 | 1 => kl.2) (p.coeff kl.1)
Ring.add_choose_eq 📋 Mathlib.RingTheory.Binomial
{R : Type u_1} [Ring R] [BinomialRing R] {r s : R} (k : ℕ) (h : Commute r s) : Ring.choose (r + s) k = ∑ ij ∈ Finset.antidiagonal k, Ring.choose r ij.1 * Ring.choose s ij.2
Ring.descPochhammer_smeval_add 📋 Mathlib.RingTheory.Binomial
{R : Type u_1} [Ring R] {r s : R} (k : ℕ) (h : Commute r s) : (descPochhammer ℤ k).smeval (r + s) = ∑ ij ∈ Finset.antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
Nat.bell_succ' 📋 Mathlib.Combinatorics.Enumerative.Bell
(n : ℕ) : (n + 1).bell = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 * ij.2.bell
catalan_succ' 📋 Mathlib.Combinatorics.Enumerative.Catalan
(n : ℕ) : catalan (n + 1) = ∑ ij ∈ Finset.antidiagonal n, catalan ij.1 * catalan ij.2
Tree.treesOfNumNodesEq_succ 📋 Mathlib.Combinatorics.Enumerative.Catalan
(n : ℕ) : Tree.treesOfNumNodesEq (n + 1) = (Finset.antidiagonal n).biUnion fun ij => Tree.pairwiseNode (Tree.treesOfNumNodesEq ij.1) (Tree.treesOfNumNodesEq ij.2)
Tree.treesOfNumNodesEq.eq_2 📋 Mathlib.Combinatorics.Enumerative.Catalan
(n : ℕ) : Tree.treesOfNumNodesEq n.succ = (Finset.antidiagonal n).attach.biUnion fun ijh => Tree.pairwiseNode (Tree.treesOfNumNodesEq (↑ijh).1) (Tree.treesOfNumNodesEq (↑ijh).2)
Tree.treesOfNumNodesEq.eq_def 📋 Mathlib.Combinatorics.Enumerative.Catalan
(x✝ : ℕ) : Tree.treesOfNumNodesEq x✝ = match x✝ with | 0 => {Tree.nil} | n.succ => (Finset.antidiagonal n).attach.biUnion fun ijh => Tree.pairwiseNode (Tree.treesOfNumNodesEq (↑ijh).1) (Tree.treesOfNumNodesEq (↑ijh).2)
MvPowerSeries.coeff_mul 📋 Mathlib.RingTheory.MvPowerSeries.Basic
{σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ℕ) (φ ψ : MvPowerSeries σ R) [DecidableEq σ] : (MvPowerSeries.coeff n) (φ * ψ) = ∑ p ∈ Finset.antidiagonal n, (MvPowerSeries.coeff p.1) φ * (MvPowerSeries.coeff p.2) ψ
PowerSeries.coeff_mul 📋 Mathlib.RingTheory.PowerSeries.Basic
{R : Type u_1} [Semiring R] (n : ℕ) (φ ψ : PowerSeries R) : (PowerSeries.coeff n) (φ * ψ) = ∑ p ∈ Finset.antidiagonal n, (PowerSeries.coeff p.1) φ * (PowerSeries.coeff p.2) ψ
Nat.castChoose_eq 📋 Mathlib.Data.Nat.Factorial.NatCast
{A : Type u_1} [CommSemiring A] {m : ℕ} {k : ℕ × ℕ} (hm : IsUnit ↑m.factorial) (hk : k ∈ Finset.antidiagonal m) : ↑(m.choose k.1) = ↑m.factorial * Ring.inverse ↑k.1.factorial * Ring.inverse ↑k.2.factorial
MvPowerSeries.inv.aux.eq_1 📋 Mathlib.RingTheory.MvPowerSeries.Inverse
{σ : Type u_1} {R : Type u_2} [Ring R] (a : R) (φ : MvPowerSeries σ R) (x✝ : σ →₀ ℕ) : MvPowerSeries.inv.aux a φ x✝ = if x✝ = 0 then a else -a * ∑ x ∈ Finset.antidiagonal x✝, if x_1 : x.2 < x✝ then (MvPowerSeries.coeff x.1) φ * MvPowerSeries.inv.aux a φ x.2 else 0
MvPowerSeries.inv.aux.eq_def 📋 Mathlib.RingTheory.MvPowerSeries.Inverse
{σ : Type u_1} {R : Type u_2} [Ring R] (a : R) (φ : MvPowerSeries σ R) (x✝ : σ →₀ ℕ) : MvPowerSeries.inv.aux a φ x✝ = have n := x✝; if n = 0 then a else -a * ∑ x ∈ Finset.antidiagonal n, if x_1 : x.2 < n then (MvPowerSeries.coeff x.1) φ * MvPowerSeries.inv.aux a φ x.2 else 0
MvPowerSeries.coeff_inv_aux 📋 Mathlib.RingTheory.MvPowerSeries.Inverse
{σ : Type u_1} {R : Type u_2} [Ring R] [DecidableEq σ] (n : σ →₀ ℕ) (a : R) (φ : MvPowerSeries σ R) : (MvPowerSeries.coeff n) (MvPowerSeries.inv.aux a φ) = if n = 0 then a else -a * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) (MvPowerSeries.inv.aux a φ) else 0
MvPowerSeries.coeff_invOfUnit 📋 Mathlib.RingTheory.MvPowerSeries.Inverse
{σ : Type u_1} {R : Type u_2} [Ring R] [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (u : Rˣ) : (MvPowerSeries.coeff n) (φ.invOfUnit u) = if n = 0 then ↑u⁻¹ else -↑u⁻¹ * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) (φ.invOfUnit u) else 0
MvPowerSeries.coeff_inv 📋 Mathlib.RingTheory.MvPowerSeries.Inverse
{σ : Type u_1} {k : Type u_3} [Field k] [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ k) : (MvPowerSeries.coeff n) φ⁻¹ = if n = 0 then (MvPowerSeries.constantCoeff φ)⁻¹ else -(MvPowerSeries.constantCoeff φ)⁻¹ * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) φ⁻¹ else 0
PowerSeries.coeff_inv_aux 📋 Mathlib.RingTheory.PowerSeries.Inverse
{R : Type u_1} [Ring R] (n : ℕ) (a : R) (φ : PowerSeries R) : (PowerSeries.coeff n) (PowerSeries.inv.aux a φ) = if n = 0 then a else -a * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (PowerSeries.coeff x.1) φ * (PowerSeries.coeff x.2) (PowerSeries.inv.aux a φ) else 0
PowerSeries.coeff_invOfUnit 📋 Mathlib.RingTheory.PowerSeries.Inverse
{R : Type u_1} [Ring R] (n : ℕ) (φ : PowerSeries R) (u : Rˣ) : (PowerSeries.coeff n) (φ.invOfUnit u) = if n = 0 then ↑u⁻¹ else -↑u⁻¹ * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (PowerSeries.coeff x.1) φ * (PowerSeries.coeff x.2) (φ.invOfUnit u) else 0
PowerSeries.coeff_inv 📋 Mathlib.RingTheory.PowerSeries.Inverse
{k : Type u_2} [Field k] (n : ℕ) (φ : PowerSeries k) : (PowerSeries.coeff n) φ⁻¹ = if n = 0 then (PowerSeries.constantCoeff φ)⁻¹ else -(PowerSeries.constantCoeff φ)⁻¹ * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (PowerSeries.coeff x.1) φ * (PowerSeries.coeff x.2) φ⁻¹ else 0
bernoulli'_spec' 📋 Mathlib.NumberTheory.Bernoulli
(n : ℕ) : ∑ k ∈ Finset.antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1 = 1
bernoulli_spec' 📋 Mathlib.NumberTheory.Bernoulli
(n : ℕ) : ∑ k ∈ Finset.antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = if n = 0 then 1 else 0
DividedPowers.exp_add' 📋 Mathlib.RingTheory.DividedPowers.Basic
{A : Type u_1} [CommSemiring A] {a b : A} (dp : ℕ → A → A) (dp_add : ∀ (n : ℕ), dp n (a + b) = ∑ k ∈ Finset.antidiagonal n, dp k.1 a * dp k.2 b) : (PowerSeries.mk fun n => dp n (a + b)) = (PowerSeries.mk fun n => dp n a) * PowerSeries.mk fun n => dp n b
DividedPowers.dpow_add 📋 Mathlib.RingTheory.DividedPowers.Basic
{A : Type u_1} [CommSemiring A] {I : Ideal A} (self : DividedPowers I) {n : ℕ} {x y : A} : x ∈ I → y ∈ I → self.dpow n (x + y) = ∑ k ∈ Finset.antidiagonal n, self.dpow k.1 x * self.dpow k.2 y
DividedPowers.dpow_sum' 📋 Mathlib.RingTheory.DividedPowers.Basic
{A : Type u_1} [CommSemiring A] {M : Type u_2} [AddCommMonoid M] {I : AddSubmonoid M} (dpow : ℕ → M → A) (dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1) (dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.antidiagonal n, dpow k.1 x * dpow k.2 y) (dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0) {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {x : ι → M} (hx : ∀ i ∈ s, x i ∈ I) {n : ℕ} : dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
DividedPowers.mk 📋 Mathlib.RingTheory.DividedPowers.Basic
{A : Type u_1} [CommSemiring A] {I : Ideal A} (dpow : ℕ → A → A) (dpow_null : ∀ {n : ℕ} {x : A}, x ∉ I → dpow n x = 0) (dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1) (dpow_one : ∀ {x : A}, x ∈ I → dpow 1 x = x) (dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow n x ∈ I) (dpow_add : ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.antidiagonal n, dpow k.1 x * dpow k.2 y) (dpow_mul : ∀ {n : ℕ} {a x : A}, x ∈ I → dpow n (a * x) = a ^ n * dpow n x) (mul_dpow : ∀ {m n : ℕ} {x : A}, x ∈ I → dpow m x * dpow n x = ↑((m + n).choose m) * dpow (m + n) x) (dpow_comp : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow m (dpow n x) = ↑(m.uniformBell n) * dpow (m * n) x) : DividedPowers I
DividedPowers.mk.sizeOf_spec 📋 Mathlib.RingTheory.DividedPowers.Basic
{A : Type u_1} [CommSemiring A] {I : Ideal A} [SizeOf A] (dpow : ℕ → A → A) (dpow_null : ∀ {n : ℕ} {x : A}, x ∉ I → dpow n x = 0) (dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1) (dpow_one : ∀ {x : A}, x ∈ I → dpow 1 x = x) (dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow n x ∈ I) (dpow_add : ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.antidiagonal n, dpow k.1 x * dpow k.2 y) (dpow_mul : ∀ {n : ℕ} {a x : A}, x ∈ I → dpow n (a * x) = a ^ n * dpow n x) (mul_dpow : ∀ {m n : ℕ} {x : A}, x ∈ I → dpow m x * dpow n x = ↑((m + n).choose m) * dpow (m + n) x) (dpow_comp : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow m (dpow n x) = ↑(m.uniformBell n) * dpow (m * n) x) : sizeOf { dpow := dpow, dpow_null := dpow_null, dpow_zero := dpow_zero, dpow_one := dpow_one, dpow_mem := dpow_mem, dpow_add := dpow_add, dpow_mul := dpow_mul, mul_dpow := mul_dpow, dpow_comp := dpow_comp } = 1
DividedPowers.mk.injEq 📋 Mathlib.RingTheory.DividedPowers.Basic
{A : Type u_1} [CommSemiring A] {I : Ideal A} (dpow : ℕ → A → A) (dpow_null : ∀ {n : ℕ} {x : A}, x ∉ I → dpow n x = 0) (dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1) (dpow_one : ∀ {x : A}, x ∈ I → dpow 1 x = x) (dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow n x ∈ I) (dpow_add : ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.antidiagonal n, dpow k.1 x * dpow k.2 y) (dpow_mul : ∀ {n : ℕ} {a x : A}, x ∈ I → dpow n (a * x) = a ^ n * dpow n x) (mul_dpow : ∀ {m n : ℕ} {x : A}, x ∈ I → dpow m x * dpow n x = ↑((m + n).choose m) * dpow (m + n) x) (dpow_comp : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow m (dpow n x) = ↑(m.uniformBell n) * dpow (m * n) x) (dpow✝ : ℕ → A → A) (dpow_null✝ : ∀ {n : ℕ} {x : A}, x ∉ I → dpow✝ n x = 0) (dpow_zero✝ : ∀ {x : A}, x ∈ I → dpow✝ 0 x = 1) (dpow_one✝ : ∀ {x : A}, x ∈ I → dpow✝ 1 x = x) (dpow_mem✝ : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow✝ n x ∈ I) (dpow_add✝ : ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → dpow✝ n (x + y) = ∑ k ∈ Finset.antidiagonal n, dpow✝ k.1 x * dpow✝ k.2 y) (dpow_mul✝ : ∀ {n : ℕ} {a x : A}, x ∈ I → dpow✝ n (a * x) = a ^ n * dpow✝ n x) (mul_dpow✝ : ∀ {m n : ℕ} {x : A}, x ∈ I → dpow✝ m x * dpow✝ n x = ↑((m + n).choose m) * dpow✝ (m + n) x) (dpow_comp✝ : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow✝ m (dpow✝ n x) = ↑(m.uniformBell n) * dpow✝ (m * n) x) : ({ dpow := dpow, dpow_null := dpow_null, dpow_zero := dpow_zero, dpow_one := dpow_one, dpow_mem := dpow_mem, dpow_add := dpow_add, dpow_mul := dpow_mul, mul_dpow := mul_dpow, dpow_comp := dpow_comp } = { dpow := dpow✝, dpow_null := dpow_null✝, dpow_zero := dpow_zero✝, dpow_one := dpow_one✝, dpow_mem := dpow_mem✝, dpow_add := dpow_add✝, dpow_mul := dpow_mul✝, mul_dpow := mul_dpow✝, dpow_comp := dpow_comp✝ }) = (dpow = dpow✝)
DividedPowers.mk.congr_simp 📋 Mathlib.RingTheory.DividedPowers.Basic
{A : Type u_1} [CommSemiring A] {I : Ideal A} (dpow dpow✝ : ℕ → A → A) (e_dpow : dpow = dpow✝) (dpow_null : ∀ {n : ℕ} {x : A}, x ∉ I → dpow n x = 0) (dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1) (dpow_one : ∀ {x : A}, x ∈ I → dpow 1 x = x) (dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow n x ∈ I) (dpow_add : ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.antidiagonal n, dpow k.1 x * dpow k.2 y) (dpow_mul : ∀ {n : ℕ} {a x : A}, x ∈ I → dpow n (a * x) = a ^ n * dpow n x) (mul_dpow : ∀ {m n : ℕ} {x : A}, x ∈ I → dpow m x * dpow n x = ↑((m + n).choose m) * dpow (m + n) x) (dpow_comp : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow m (dpow n x) = ↑(m.uniformBell n) * dpow (m * n) x) : { dpow := dpow, dpow_null := dpow_null, dpow_zero := dpow_zero, dpow_one := dpow_one, dpow_mem := dpow_mem, dpow_add := dpow_add, dpow_mul := dpow_mul, mul_dpow := mul_dpow, dpow_comp := dpow_comp } = { dpow := dpow✝, dpow_null := ⋯, dpow_zero := ⋯, dpow_one := ⋯, dpow_mem := ⋯, dpow_add := ⋯, dpow_mul := ⋯, mul_dpow := ⋯, dpow_comp := ⋯ }
DividedPowers.OfInvertibleFactorial.dpow_add_of_lt 📋 Mathlib.RingTheory.DividedPowers.RatAlgebra
{A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun x => x ∈ I] {n : ℕ} (hn_fac : IsUnit ↑(n - 1).factorial) {m : ℕ} (hmn : m < n) {x y : A} (hx : x ∈ I) (hy : y ∈ I) : DividedPowers.OfInvertibleFactorial.dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, DividedPowers.OfInvertibleFactorial.dpow I k.1 x * DividedPowers.OfInvertibleFactorial.dpow I k.2 y
DividedPowers.OfInvertibleFactorial.dpow_add 📋 Mathlib.RingTheory.DividedPowers.RatAlgebra
{A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun x => x ∈ I] {n : ℕ} (hn_fac : IsUnit ↑(n - 1).factorial) (hnI : I ^ n = 0) {m : ℕ} {x : A} (hx : x ∈ I) {y : A} (hy : y ∈ I) : DividedPowers.OfInvertibleFactorial.dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, DividedPowers.OfInvertibleFactorial.dpow I k.1 x * DividedPowers.OfInvertibleFactorial.dpow I k.2 y
MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero 📋 Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
(σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] : ∑ a ∈ Finset.antidiagonal (Fintype.card σ), (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2 = 0
MvPolynomial.mul_esymm_eq_sum 📋 Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
(σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] (k : ℕ) : ↑k * MvPolynomial.esymm σ R k = (-1) ^ (k + 1) * ∑ a ∈ Finset.antidiagonal k with a.1 < k, (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2
MvPolynomial.psum_eq_mul_esymm_sub_sum 📋 Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
(σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] (k : ℕ) (h : 0 < k) : MvPolynomial.psum σ R k = (-1) ^ (k + 1) * ↑k * MvPolynomial.esymm σ R k - ∑ a ∈ Finset.antidiagonal k with a.1 ∈ Set.Ioo 0 k, (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision 1c119a3