Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-07 20:32 575fcc65

View on Github →

refactor(data/nat/choose): reduce assumptions on lemmas (#8508)

  • rename nat.choose_eq_factorial_div_factorial' to nat.cast_choose
  • change the cast from ℚ to any char_zero field
  • get rid of the cast in nat.choose_mul. Generalization ensues.

Estimated changes

added theorem nat.choose_mul
added theorem nat.cast_choose
deleted theorem nat.choose_mul