isRelPrime_iff_not_dvd — Mathlib

English

Let p be irreducible. Then p is relatively prime to n if and only if p does not divide n.

Русский

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

LaTeX

$$$$\mathrm{Irreducible}(p) \Rightarrow (\mathrm{IsRelPrime}(p,n) \iff \neg (p \mid n)).$$$$

Lean4

/-- See also `Irreducible.coprime_iff_not_dvd`. -/
theorem isRelPrime_iff_not_dvd [Monoid M] {p n : M} (hp : Irreducible p) : IsRelPrime p n ↔ ¬p ∣ n :=
  by
  refine ⟨fun h contra ↦ hp.not_isUnit (h dvd_rfl contra), fun hpn d hdp hdn ↦ ?_⟩
  contrapose! hpn
  suffices Associated p d from this.dvd.trans hdn
  exact (hp.dvd_iff.mp hdp).resolve_left hpn

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