factorization — Mathlib

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

Похожие утверждения