Theorem Finset.Nat.sum_antidiagonal_succ

Modification history

2026-08-15 23:59

Mathlib/Algebra/BigOperators/NatAntidiagonal.lean

chore(Algebra/BigOperators): add to_additive for expectation and antidiagonal lemmas (#42763) …

Deleted Finset.Nat.sum_antidiagonal_succ View on Github →

2023-01-19 06:52

Mathlib/Algebra/BigOperators/NatAntidiagonal.lean

feat port: Algebra.BigOperators.NatAntidiagonal (#1656)

Added Finset.Nat.sum_antidiagonal_succ View on Github →