Theorem Nat.Ico_pow_dvd_eq_Ico_of_lt

Modification history

2025-08-09 19:57
Mathlib/Data/Nat/Factorization/Basic.lean
chore: deduce `Nat.multiplicity` lemmas from the `Nat.factorization` ones (#22503) …
Added Nat.Ico_pow_dvd_eq_Ico_of_ltView on Github →