English
For a prime p and n > 0, the set { i ∈ ℕ | 1 ≤ i ≤ v_p(n) } equals { i ∈ ℕ | i ∈ Ico(1, n) and p^i | n }.
Русский
Для простого p и n > 0 множество { i ∈ ℕ | 1 ≤ i ≤ v_p(n) } совпадает с { i ∈ ℕ | i ∈ Ico(1, n) и p^i | n }.
LaTeX
$$$ \mathrm{Icc}(1, n.factorization p) = \{ i \in \mathrm{Ico}(1, n) \mid p^i \mid n \} $$$
Lean4
/-- The set of positive powers of prime `p` that divide `n` is exactly the set of
positive natural numbers up to `n.factorization p`. -/
theorem Icc_factorization_eq_pow_dvd (n : ℕ) {p : ℕ} (pp : Prime p) :
Icc 1 (n.factorization p) = {i ∈ Ico 1 n | p ^ i ∣ n} :=
by
rcases eq_or_ne n 0 with (rfl | hn)
· simp
ext x
simp only [mem_Icc, Finset.mem_filter, mem_Ico, and_assoc, and_congr_right_iff, pp.pow_dvd_iff_le_factorization hn,
iff_and_self]
exact fun _ H => lt_of_le_of_lt H (factorization_lt p hn)
