gcd_dvd_iff_exists — Mathlib

English

For a,b in a Bézout ring, and any z, gcd(a,b) divides z iff z can be expressed as a linear combination of a and b.

Русский

Для a,b в кольце Безоу, и любого z, gcd(a,b) делит z тогда и только тогда, когда z можно выразить как линейную комбинацию a и b.

LaTeX

$$$\forall a,b \in R, \; \gcd(a,b) \mid z \iff \exists x,y, z = a \cdot x + b \cdot y$$$

Lean4

theorem gcd_dvd_iff_exists (a b : R) {z} : gcd a b ∣ z ↔ ∃ x y, z = a * x + b * y := by
  simp_rw [mul_comm a, mul_comm b, @eq_comm _ z, ← Ideal.mem_span_pair, ← span_gcd, Ideal.mem_span_singleton]

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