prime_of_mem_primeFactorsList — Mathlib

English

If p ∈ primeFactorsList n, then p is prime.

Русский

Если p принадлежит списку primeFactorsList n, то p — простое.

LaTeX

$$$ \forall {n,p},\ p \in \text{primeFactorsList}(n) \Rightarrow \text{Prime}(p) $$$

Lean4

theorem prime_of_mem_primeFactorsList {n : ℕ} : ∀ {p : ℕ}, p ∈ primeFactorsList n → Prime p := by
  match n with
  | 0 => simp
  | 1 => simp
  | k + 2 =>
    intro p h
    let m := minFac (k + 2)
    have : (k + 2) / m < (k + 2) := factors_lemma
    have h₁ : p = m ∨ p ∈ primeFactorsList ((k + 2) / m) := List.mem_cons.1 (by rwa [primeFactorsList] at h)
    exact Or.casesOn h₁ (fun h₂ => h₂.symm ▸ minFac_prime (by simp)) prime_of_mem_primeFactorsList

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