dvd_prime — Mathlib

English

For a prime p, every divisor m of p is either 1 or p.

Русский

Для простого p любой делитель m числа p равен 1 или p.

LaTeX

$$$\\\\mathrm{Prime}(p) \\\\rightarrow (\\\\forall m \\\\; (m \\\\mid p \\\\rightarrow (m = 1 \\\\lor m = p)))$$$

Lean4

theorem dvd_prime {p m : ℕ} (pp : Prime p) : m ∣ p ↔ m = 1 ∨ m = p :=
  ⟨fun d => pp.eq_one_or_self_of_dvd m d, fun h => h.elim (fun e => e.symm ▸ one_dvd _) fun e => e.symm ▸ dvd_rfl⟩

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