Commit 2025-10-31 09:48 025eb7b8

View on Github →

chore(Data/Nat/{Factorial, Choose}/Cast): move lemmas about Polynomial (#30745) The remaining lemmas in the files are unrelated to ascPochhammer and descPochhammer. This significantly reduces the imports.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Pochhammer.lean

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

deleted theorem Nat.cast_choose_eq_ascPochhammer_div

deleted theorem Nat.cast_choose_eq_descPochhammer_div

Modified Mathlib/Data/Nat/Factorial/Cast.lean

deleted theorem Nat.cast_ascFactorial

deleted theorem Nat.cast_descFactorial

deleted theorem Nat.cast_factorial

Modified Mathlib/RingTheory/Polynomial/Pochhammer.lean

added theorem Nat.cast_ascFactorial

added theorem Nat.cast_choose_eq_ascPochhammer_div

added theorem Nat.cast_choose_eq_descPochhammer_div

added theorem Nat.cast_descFactorial

added theorem Nat.cast_factorial