prime_def_le_sqrt — Mathlib

English

Prime p iff p ≥ 2 and ∀ m < p, m ∣ p → m = 1.

Русский

Простое число p эквивалентно p ≥ 2 и ∀ m < p, если m ∣ 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_le_sqrt {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m, 2 ≤ m → m ≤ sqrt p → ¬m ∣ p :=
  prime_def_lt'.trans <|
    and_congr_right fun p2 =>
      ⟨fun a m m2 l => a m m2 <| lt_of_le_of_lt l <| sqrt_lt_self p2, fun a m m2 l mdvd@⟨k, e⟩ =>
        by
        rcases le_sqrt_of_eq_mul e with hm | hk
        · exact a m m2 hm mdvd
        · rw [mul_comm] at e
          exact a k (Nat.lt_of_mul_lt_mul_right (a := m) (by rwa [one_mul, ← e])) hk ⟨m, e⟩⟩

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