Antidiagonal

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

Statistics

Metric	Count
Definitions antidiagonal', instHasAntidiagonal	2
Theorems antidiagonal_single, antidiagonal_zero, prod_antidiagonal_swap, sum_antidiagonal_swap	4
Total	6

Finsupp

Definitions

Name	Category	Theorems
antidiagonal' 📖	CompOp	—
instHasAntidiagonal 📖	CompOp	11 math math: 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	—	—
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