mathlib3

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

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.