Theorem Nat.add_one_mul_choose_eq

Modification history

2025-12-10 02:48

Mathlib/Data/Nat/Choose/Basic.lean

chore: deprecate Nat.succ_mul_choose_eq (#32653)

Modified Nat.add_one_mul_choose_eq View on Github →

2025-12-09 14:57

Mathlib/Data/Nat/Choose/Basic.lean

feat: lemmas about `Polynomial.bernoulli` and `bernoulliFun` (#32364) …

Added Nat.add_one_mul_choose_eq View on Github →