coprime_iff_not_dvd — Mathlib

English

Let p be prime. Then IsCoprime p n iff p does not divide n.

Русский

Пусть p — простое. Тогда IsCoprime(p,n) эквивалентно тому, что p не делит n.

LaTeX

$$$\forall {R} [\mathrm{CommRing}\,R] [\mathrm{IsBezout}\,R] {p n : R} (hp : \mathrm{Prime}(p)) : \mathrm{IsCoprime}(p,n) \iff \neg (p \mid n)$$$

Lean4

theorem coprime_iff_not_dvd {p n : R} (hp : Prime p) : IsCoprime p n ↔ ¬p ∣ n :=
  hp.irreducible.coprime_iff_not_dvd

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