prime_dvd_prime_iff_eq — Mathlib

English

Let p and q be primes. Then p ∣ q if and only if p = q.

Русский

Пусть p и q — простые числа. Тогда p делит q тогда же, когда p = q.

LaTeX

$$$\\\\forall p,q \\\\in \\\\mathbb{N}, \\\\mathrm{Prime}(p) \\\\land \\\\mathrm{Prime}(q) \\\\rightarrow (p \\\\mid q) \\\\\\leftrightarrow (p = q).$$$

Lean4

theorem prime_dvd_prime_iff_eq {p q : ℕ} (pp : p.Prime) (qp : q.Prime) : p ∣ q ↔ p = q :=
  dvd_prime_two_le qp (Prime.two_le pp)

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