eq_or_coprime_of_le_prime — Mathlib

English

For n,p with n ≠ 0 ≤ p and p prime, either p = n or p and n are coprime.

Русский

Для n,p с n ≠ 0 и n ≤ p, p простое: либо p = n, либо p и n взаимно просты.

LaTeX

$$$$ \forall p,n \in \mathbb{N},\ n \neq 0 \land n \le p \land \text{Prime}(p) \Rightarrow p = n \lor \gcd(p,n) = 1. $$$$

Lean4

theorem eq_or_coprime_of_le_prime {n p} (ne_zero : n ≠ 0) (hle : n ≤ p) (pp : Prime p) : p = n ∨ Coprime p n :=
  hle.eq_or_lt.imp Eq.symm fun h => coprime_of_lt_prime ne_zero h pp

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