exists_gcd_eq_mul_add_mul

Mathlib.RingTheory.PrincipalIdealDomain

URI: https://scilib.ai/kg/mathlib#exists_gcd_eq_mul_add_mul

English

There exist x,y such that gcd(a,b) = a x + b y ( Bézout's lemma ).

Русский

Существуют x,y такие, что gcd(a,b) = a x + b y ( лемма Безоу ).

LaTeX

$$$\exists x,y \; \gcd(a,b) = a x + b y$$$

Lean4

/-- **Bézout's lemma** -/
theorem exists_gcd_eq_mul_add_mul (a b : R) : ∃ x y, gcd a b = a * x + b * y := by rw [← gcd_dvd_iff_exists]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru