gcd_dvd_left — Mathlib

English

Let R be a commutative ring and x, y ∈ R with the property that the ideal generated by x and y is principal. Then gcd(x, y) divides x.

Русский

Пусть R — коммутативное кольцо и элементы x, y ∈ R такие, что идеал, порожденный x и y, является главной. Тогда gcd(x, y) делит x.

LaTeX

$$$\\\\gcd(x,y) \\\\mid x$$$

Lean4

theorem gcd_dvd_left : gcd x y ∣ x :=
  (Submodule.IsPrincipal.mem_iff_generator_dvd _).mp (Ideal.subset_span (by simp))

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