Commit 2023-01-19 06:52 da5db4bb

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/BigOperators/NatAntidiagonal.lean

added theorem Finset.Nat.prod_antidiagonal_eq_prod_range_succ

added theorem Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk

added theorem Finset.Nat.prod_antidiagonal_subst

added theorem Finset.Nat.prod_antidiagonal_succ'

added theorem Finset.Nat.prod_antidiagonal_succ

added theorem Finset.Nat.prod_antidiagonal_swap

added theorem Finset.Nat.sum_antidiagonal_succ'

added theorem Finset.Nat.sum_antidiagonal_succ