dvd_iff_not_isCoprime — Mathlib

English

If p is irreducible, then p divides n if and only if p and n are not coprime.

Русский

Если p неприводимо, то p делит n тогда, когда p и n не взаимно просты.

LaTeX

$$$\forall {R} [\mathrm{CommRing}\,R] [\mathrm{IsBezout}\,R] {p n : R} \; (p \text{ Irreducible}) \Rightarrow (p \mid n) \iff \lnot \mathrm{IsCoprime}(p,n)$$$

Lean4

/-- See also `Irreducible.coprime_iff_not_dvd'`. -/
theorem dvd_iff_not_isCoprime {p n : R} (hp : Irreducible p) : p ∣ n ↔ ¬IsCoprime p n :=
  iff_not_comm.2 hp.coprime_iff_not_dvd

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