primeFactorsList_prime — Mathlib

English

If p is prime, then primeFactorsList p = [p].

Русский

Если p простое, то primeFactorsList p = [p].

LaTeX

$$$ \forall p,\ \text{Nat.Prime}(p) \Rightarrow \text{primeFactorsList}(p) = [p] $$$

Lean4

theorem primeFactorsList_prime {p : ℕ} (hp : Nat.Prime p) : p.primeFactorsList = [p] :=
  by
  have : p = p - 2 + 2 := Nat.eq_add_of_sub_eq hp.two_le rfl
  rw [this, primeFactorsList]
  simp only [Eq.symm this]
  have : Nat.minFac p = p := (Nat.prime_def_minFac.mp hp).2
  simp only [this, primeFactorsList, Nat.div_self (Nat.Prime.pos hp)]

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