prime_def_minFac — Mathlib

English

Prime p is equivalent to 2 ≤ p and minFac p = p.

Русский

Простое p эквивалентно 2 ≤ p и minFac p = p.

LaTeX

$$$\\\\mathrm{Prime}(p) \\\\\\Leftrightarrow \\\\bigl(2 \\\\\\le p \\\\land \\\\minFac(p) = p\\\\bigr).$$$

Lean4

theorem prime_def_minFac {p : ℕ} : Prime p ↔ 2 ≤ p ∧ minFac p = p :=
  ⟨fun pp =>
    ⟨pp.two_le,
      let ⟨f2, fd, _⟩ := minFac_has_prop <| ne_of_gt pp.one_lt
      ((dvd_prime pp).1 fd).resolve_left (ne_of_gt f2)⟩,
    fun ⟨p2, e⟩ => e ▸ minFac_prime (ne_of_gt p2)⟩

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