isCoprime_or_dvd — Mathlib

English

If p is irreducible, then for any i, either p is coprime to i or p divides i.

Русский

Если p неприводимо, то для любого i либо p взаимно просто с i, либо p делит i.

LaTeX

$$$\forall {R} [\mathrm{CommRing}\,R] [\mathrm{IsBezout}\,R] {p : R} (i : R) (hp : \mathrm{Irreducible}(p)), \; \mathrm{IsCoprime}(p,i) \lor p \mid i$$$

Lean4

theorem isCoprime_or_dvd {p : R} (hp : Irreducible p) (i : R) : IsCoprime p i ∨ p ∣ i :=
  (_root_.em _).imp_right hp.dvd_iff_not_isCoprime.2

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