English
Prime p iff p ≥ 2 and every divisor m of p is either 1 or p.
Русский
Пусть p — простое число тогда и только тогда, когда p ≥ 2 и каждый делитель m числа p равен 1 или p.
LaTeX
$$$\\\\mathrm{Prime}(p) \\\\iff 2 \\\\le p \\\\land \\\\forall m, \\\\; m \\\\mid p \\\\rightarrow m = 1 \\\\lor m = p$$$
Lean4
@[inherit_doc Nat.Prime]
theorem prime_def {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m, m ∣ p → m = 1 ∨ m = p :=
by
refine ⟨fun h => ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, fun h => ?_⟩
have h1 := Nat.one_lt_two.trans_le h.1
refine ⟨mt Nat.isUnit_iff.mp h1.ne', ?_⟩
rintro a b rfl
simp only [Nat.isUnit_iff]
refine (h.2 a <| dvd_mul_right ..).imp_right fun hab ↦ ?_
rw [← mul_right_inj' (Nat.ne_zero_of_lt h1), ← hab, ← hab, mul_one]
