English
If p is prime, its factorization is the single prime factor p with exponent 1.
Русский
Если p — простое число, то факторизация p равна единственному простому фактору p с показателем 1.
LaTeX
$$$\\text{Prime}(p) \\Rightarrow p.factorization = \\mathrm{single}\\ p\\ 1$$$
Lean4
/-- The only prime factor of prime `p` is `p` itself, with multiplicity `1` -/
@[simp]
protected theorem factorization {p : ℕ} (hp : Prime p) : p.factorization = single p 1 :=
by
ext q
rw [← primeFactorsList_count_eq, primeFactorsList_prime hp, single_apply, count_singleton', if_congr eq_comm] <;> rfl