prime_def_lt — Mathlib

English

Prime p iff p ≥ 2 and every divisor m < p, with m | p, satisfies m = 1.

Русский

Простое число p эквивалентно p ≥ 2 и каждому делителю m < p, делящему p, выполняется m = 1.

LaTeX

$$$\\\\mathrm{Prime}(p) \\\\iff 2 \\\\le p \\\\land \\\\forall m < p, \\\\; m \\\\mid p \\\\rightarrow m = 1$$$

Lean4

theorem prime_def_lt {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m < p, m ∣ p → m = 1 :=
  prime_def.trans <|
    and_congr_right fun p2 =>
      forall_congr' fun _ =>
        ⟨fun h l d => (h d).resolve_right (ne_of_lt l), fun h d =>
          (le_of_dvd (le_of_succ_le p2) d).lt_or_eq_dec.imp_left fun l => h l d⟩

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