Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-26 14:35 255bebc0

View on Github →

feat(data/nat/multiplicity): multiplicity_choose and others (#1704)

Estimated changes

Modified src/data/nat/modeq.lean

added theorem nat.le_mod_add_mod_of_dvd_add_of_not_dvd

Created src/data/nat/multiplicity.lean

added theorem nat.multiplicity_eq_card_pow_dvd

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_fact

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_fact_iff