dvd_gcd — 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 dvd_gcd (hx : z ∣ x) (hy : z ∣ y) : z ∣ gcd x y :=
  by
  rw [← Ideal.span_singleton_le_span_singleton] at hx hy ⊢
  rw [span_gcd, Ideal.span_insert, sup_le_iff]
  exact ⟨hx, hy⟩

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