dvd_or_coprime — Mathlib

English

For any two elements in a Euclidean domain, an irreducible element either divides one of them or the pair is coprime. This is a standard dichotomy used in gcd theory.

Русский

Для любых двух элементов в евклидовом домене неприводимый элемент либо делит одно из них, либо пара взаимно проста. Это стандартная дихотомия теории gcd.

LaTeX

$$$\\text{dvd or coprime}(x,y)$: either d|x for some irreducible d or IsCoprime(x,y).$$

Lean4

theorem dvd_or_coprime (x y : α) (h : Irreducible x) : x ∣ y ∨ IsCoprime x y :=
  letI := Classical.decEq α
  letI := EuclideanDomain.gcdMonoid α
  _root_.dvd_or_isCoprime x y h

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