prime_of_coprime — Mathlib

English

If n > 1 and for all m < n we have gcd(n,m) = 1, then n is prime.

Русский

Если n > 1 и для каждого m < n gcd(n,m) = 1, то n — простое.

LaTeX

$$$\\\\forall n \\\\; (1 < n) \\\\land \\\\forall m < n, m \\\\neq 0 \\\\rightarrow \\\\mathrm{Coprime}(n,m) \\\\rightarrow \\\\mathrm{Prime}(n)$$$

Lean4

theorem prime_of_coprime (n : ℕ) (h1 : 1 < n) (h : ∀ m < n, m ≠ 0 → n.Coprime m) : Prime n :=
  by
  refine prime_def_lt.mpr ⟨h1, fun m mlt mdvd => ?_⟩
  have hm : m ≠ 0 := by
    rintro rfl
    rw [zero_dvd_iff] at mdvd
    exact mlt.ne' mdvd
  exact (h m mlt hm).symm.eq_one_of_dvd mdvd

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