gcd_dvd_right — 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 y.

Русский

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

LaTeX

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

Lean4

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

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