span_gcd_eq_span_gcd — Mathlib

English

In a Bézout ring with domain property, the span generated by gcd(x,y) equals the span generated by x and y.

Русский

В кольце Безоу с дополнительным свойством домена порождаемые НОД равны порождаемой парой x,y.

LaTeX

$$$\forall x,y\in R,\; \mathrm{span}\{\gcd(x,y)\} = \mathrm{span}\{x,y\}$$$

Lean4

theorem span_gcd_eq_span_gcd (x y : R) : span {GCDMonoid.gcd x y} = span {IsBezout.gcd x y} :=
  by
  rw [Ideal.span_singleton_eq_span_singleton]
  exact
    associated_of_dvd_dvd (IsBezout.dvd_gcd (GCDMonoid.gcd_dvd_left _ _) <| GCDMonoid.gcd_dvd_right _ _)
      (GCDMonoid.dvd_gcd (IsBezout.gcd_dvd_left _ _) <| IsBezout.gcd_dvd_right _ _)

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