Commit 2025-12-10 02:48 21c6094b

View on Github →

chore: deprecate Nat.succ_mul_choose_eq (#32653)

Estimated changes

Modified Archive/Wiedijk100Theorems/BallotProblem.lean

Modified Mathlib/Algebra/Polynomial/Eval/Degree.lean

Modified Mathlib/Data/Nat/Choose/Basic.lean

modified theorem Nat.add_one_mul_choose_eq

modified theorem Nat.succ_mul_choose_eq

Modified Mathlib/Data/Nat/Choose/Factorization.lean

Modified Mathlib/Data/Nat/Choose/Multinomial.lean

Modified Mathlib/Data/Nat/Multiplicity.lean

Modified Mathlib/RingTheory/Polynomial/Bernstein.lean