English
The count of p in the primeFactorsList equals the p-coordinate of n.factorization.
Русский
Число вхождений p в primeFactorsList равно p-координате n.factorization.
LaTeX
$$[simp] Theorem primeFactorsList_count_eq: n.primeFactorsList.count p = n.factorization p$$
Lean4
/-- We can write both `n.factorization p` and `n.factors.count p` to represent the power
of `p` in the factorization of `n`: we declare the former to be the simp-normal form. -/
@[simp]
theorem primeFactorsList_count_eq {n p : ℕ} : n.primeFactorsList.count p = n.factorization p :=
by
rcases n.eq_zero_or_pos with (rfl | hn0)
· simp [factorization, count]
if pp : p.Prime then ?_
else
rw [count_eq_zero_of_not_mem (mt prime_of_mem_primeFactorsList pp)]
simp [factorization, pp]
simp only [factorization_def _ pp]
apply _root_.le_antisymm
· rw [le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne']
exact List.replicate_sublist_iff.mpr le_rfl |>.subperm
· rw [← Nat.lt_add_one_iff, lt_iff_not_ge, le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne']
intro h
have := h.count_le p
simp at this
