Antidiagonal

📁 Source: Mathlib/Data/Finsupp/Antidiagonal.lean

Statistics

Metric	Count
Definitions antidiagonal', instHasAntidiagonal	2
Theorems antidiagonal_single, antidiagonal_zero, image_prodMap_embDomain_antidiagonal, prod_antidiagonal_swap, sum_antidiagonal_swap	5
Total	7

Finsupp

Definitions

Name	Category	Theorems
antidiagonal' 📖	CompOp	—
instHasAntidiagonal 📖	CompOp	12 math math: image_prodMap_embDomain_antidiagonal, MvPowerSeries.coeff_pow, antidiagonal_single, MvPowerSeries.coeff_inv, MvPowerSeries.coeff_inv_aux, MvPowerSeries.coeff_prod, sum_antidiagonal_swap, antidiagonal_zero, MvPowerSeries.coeff_invOfUnit, prod_antidiagonal_swap, MvPolynomial.coeff_mul, MvPowerSeries.coeff_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antidiagonal_single 📖	mathematical	—	Finset.HasAntidiagonal.antidiagonal Finsupp MulZeroClass.toZero Nat.instMulZeroClass instAddMonoid Nat.instAddMonoid instHasAntidiagonal single Finset.map Function.Embedding.prodMap single_injective Finset.Nat.instHasAntidiagonal	—	Finset.ext single_injective DFunLike.congr_fun single_eq_same single_apply Decidable.eq_or_ne Unique.instSubsingleton single_add
antidiagonal_zero 📖	mathematical	—	Finset.HasAntidiagonal.antidiagonal Finsupp MulZeroClass.toZero Nat.instMulZeroClass instAddMonoid Nat.instAddMonoid instHasAntidiagonal instZero Finset Finset.instSingleton	—	—
image_prodMap_embDomain_antidiagonal 📖	mathematical	—	Finset.image Finsupp MulZeroClass.toZero Nat.instMulZeroClass instDecidableEq embDomain Finset.HasAntidiagonal.antidiagonal instAddMonoid Nat.instAddMonoid instHasAntidiagonal	—	Finset.ext embDomain_add Function.Injective.injOn Function.Embedding.injective comapDomain_add_of_injective comapDomain_embDomain embDomain_comapDomain mem_range_embDomain_iff isLowerSet_range_embDomain le_iff_exists_add instCanonicallyOrderedAddOfAddLeftMono Nat.instCanonicallyOrderedAdd Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid le_iff_exists_add'
prod_antidiagonal_swap 📖	mathematical	—	Finset.prod Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.HasAntidiagonal.antidiagonal instAddMonoid Nat.instAddMonoid instHasAntidiagonal	—	Finset.prod_equiv add_comm
sum_antidiagonal_swap 📖	mathematical	—	Finset.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.HasAntidiagonal.antidiagonal instAddMonoid Nat.instAddMonoid instHasAntidiagonal	—	Finset.sum_equiv Finset.HasAntidiagonal.mem_antidiagonal add_comm

---

← Back to Index