coprime_iff_not_dvd — Mathlib

English

Let p be irreducible in a Bézout ring. Then p is coprime to n if and only if p does not divide n.

Русский

Пусть p в кольце Безоу неприводимо. Тогда p взаимно просто с n тогда и только тогда, когда p не делит n.

LaTeX

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

Lean4

/-- See also `Irreducible.isRelPrime_iff_not_dvd`. -/
theorem coprime_iff_not_dvd {p n : R} (hp : Irreducible p) : IsCoprime p n ↔ ¬p ∣ n := by
  rw [← isRelPrime_iff_isCoprime, hp.isRelPrime_iff_not_dvd]

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