Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-27 10:42 114ff8a4

View on Github →

feat(data/nat/multiplicity): rename nat.multiplicity_choose_prime_pow, add lemmas (#18183)

  • Rename nat.multiplicity_choose_prime_pow to nat.multiplicity_choose_prime_pow_add_multiplicity.
  • Add part_enat.eq_coe_sub_of_add_eq_coe and a version of nat.multiplicity_choose_prime_pow with just the multiplicity of p in choose (p ^ n) k in the LHS.
  • Golf 2 proofs.

Estimated changes