NatAntidiagonal

📁 Source: Mathlib/Algebra/BigOperators/NatAntidiagonal.lean

Statistics

Metric	Count
Definitions	0
Theorems prod_antidiagonal_eq_prod_range_succ, prod_antidiagonal_eq_prod_range_succ_mk, prod_antidiagonal_subst, prod_antidiagonal_succ, prod_antidiagonal_succ', prod_antidiagonal_swap, sum_antidiagonal_eq_sum_range_succ, sum_antidiagonal_eq_sum_range_succ_mk, sum_antidiagonal_subst, sum_antidiagonal_succ, sum_antidiagonal_succ', sum_antidiagonal_swap	12
Total	12

Finset.Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_antidiagonal_eq_prod_range_succ 📖	mathematical	—	Finset.prod Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid instHasAntidiagonal Finset.range	—	—
prod_antidiagonal_eq_prod_range_succ_mk 📖	mathematical	—	Finset.prod Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid instHasAntidiagonal Finset.range	—	Finset.prod_map
prod_antidiagonal_subst 📖	mathematical	—	Finset.prod Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid instHasAntidiagonal	—	Finset.prod_congr Finset.HasAntidiagonal.mem_antidiagonal
prod_antidiagonal_succ 📖	mathematical	—	Finset.prod Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid instHasAntidiagonal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Nat.succ_injective antidiagonal_succ Finset.prod_cons Finset.prod_map
prod_antidiagonal_succ' 📖	mathematical	—	Finset.prod Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid instHasAntidiagonal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	prod_antidiagonal_swap prod_antidiagonal_succ
prod_antidiagonal_swap 📖	mathematical	—	Finset.prod Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid instHasAntidiagonal	—	Prod.swap_injective Finset.map_swap_antidiagonal Finset.prod_map
sum_antidiagonal_eq_sum_range_succ 📖	mathematical	—	Finset.sum Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid instHasAntidiagonal Finset.range	—	—
sum_antidiagonal_eq_sum_range_succ_mk 📖	mathematical	—	Finset.sum Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid instHasAntidiagonal Finset.range	—	Finset.sum_map
sum_antidiagonal_subst 📖	mathematical	—	Finset.sum Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid instHasAntidiagonal	—	Finset.sum_congr Finset.HasAntidiagonal.mem_antidiagonal
sum_antidiagonal_succ 📖	mathematical	—	Finset.sum Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid instHasAntidiagonal AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	prod_antidiagonal_succ
sum_antidiagonal_succ' 📖	mathematical	—	Finset.sum Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid instHasAntidiagonal AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	prod_antidiagonal_succ'
sum_antidiagonal_swap 📖	mathematical	—	Finset.sum Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid instHasAntidiagonal	—	Prod.swap_injective Finset.map_swap_antidiagonal Finset.sum_map

---

← Back to Index