Commit 2023-03-19 13:50 9773c735

View on Github →

feat: port Data.Nat.Multiplicity (#2974)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Multiplicity.lean

added theorem Nat.Prime.dvd_choose_pow

added theorem Nat.Prime.dvd_choose_pow_iff

added theorem Nat.Prime.multiplicity_choose

added theorem Nat.Prime.multiplicity_choose_aux

added theorem Nat.Prime.multiplicity_choose_prime_pow

added theorem Nat.Prime.multiplicity_choose_prime_pow_add_multiplicity

added theorem Nat.Prime.multiplicity_factorial

added theorem Nat.Prime.multiplicity_factorial_le_div_pred

added theorem Nat.Prime.multiplicity_factorial_mul

added theorem Nat.Prime.multiplicity_factorial_mul_succ

added theorem Nat.Prime.multiplicity_le_multiplicity_choose_add

added theorem Nat.Prime.multiplicity_mul

added theorem Nat.Prime.multiplicity_one

added theorem Nat.Prime.multiplicity_pow

added theorem Nat.Prime.multiplicity_pow_self

added theorem Nat.Prime.multiplicity_self

added theorem Nat.Prime.pow_dvd_factorial_iff

added theorem Nat.multiplicity_eq_card_pow_dvd

added theorem Nat.multiplicity_two_factorial_lt