gcd_eq_sum

Mathlib.RingTheory.PrincipalIdealDomain

URI: https://scilib.ai/kg/mathlib#IsBezout.gcd_eq_sum

English

There exist a, b ∈ R such that a x + b y = gcd(x, y).

Русский

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

LaTeX

$$$\\\\exists a,b \\\\in R:\\ a x + b y = \\\\gcd(x,y)$$$

Lean4

theorem gcd_eq_sum : ∃ a b : R, a * x + b * y = gcd x y :=
  Ideal.mem_span_pair.mp (by rw [← span_gcd]; apply Ideal.subset_span; simp)

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

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

Разделы

Аффилиация

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