Commit 2025-08-09 19:57 01e17174

View on Github →

chore: deduce Nat.multiplicity lemmas from the Nat.factorization ones (#22503) Port lemmas from Data/Nat/Multiplicity to into a new file called Data/Nat/Factorization/Multiplicity, re-written in terms of factorization.

Estimated changes

Modified Mathlib/Data/Nat/Choose/Factorization.lean

added theorem Nat.factorization_choose'

added theorem Nat.factorization_choose

added theorem Nat.factorization_choose_prime_pow

added theorem Nat.factorization_choose_prime_pow_add_factorization

added theorem Nat.factorization_factorial

added theorem Nat.factorization_factorial_le_div_pred

added theorem Nat.factorization_factorial_mul

added theorem Nat.factorization_factorial_mul_succ

added theorem Nat.factorization_le_factorization_choose_add

added theorem Nat.factorization_le_factorization_of_dvd_right

added theorem Nat.multiplicity_choose_aux

added theorem Nat.sub_one_mul_factorization_factorial

Modified Mathlib/Data/Nat/Factorization/Basic.lean

added theorem Nat.Ico_pow_dvd_eq_Ico_of_lt

added theorem Nat.factorization_eq_card_pow_dvd_of_lt

added theorem Nat.factorization_pow_self

added theorem Nat.factorization_prod_apply

Modified Mathlib/Data/Nat/Multiplicity.lean

deleted theorem Nat.Prime.multiplicity_choose_aux