English
For m ∈ ℕ+ and p a prime, and k ∈ ℕ, p^k divides m if and only if k is at most the multiplicity of p in m.factorMultiset.
Русский
Для m ∈ ℕ+ и простого p и натурального k, p^k делит m тогда и только тогда, когда k не превосходит кратность p в m.factorMultiset.
LaTeX
$$$ (p)^k \\mid m \\iff k \\le \\operatorname{count}(p, m.\\operatorname{factorMultiset}) $$$
Lean4
/-- The number of occurrences of p in the factor multiset of m
is the same as the p-adic valuation of m. -/
theorem count_factorMultiset (m : ℕ+) (p : Nat.Primes) (k : ℕ) : (p : ℕ+) ^ k ∣ m ↔ k ≤ m.factorMultiset.count p :=
by
rw [Multiset.le_count_iff_replicate_le, ← factorMultiset_le_iff, factorMultiset_pow, factorMultiset_ofPrime]
congr! 2
apply Multiset.eq_replicate.mpr
constructor
· rw [Multiset.card_nsmul, PrimeMultiset.card_ofPrime, mul_one]
· intro q h
rw [PrimeMultiset.ofPrime, Multiset.nsmul_singleton _ k] at h
exact Multiset.eq_of_mem_replicate h
