gcd_rel_right

Mathlib.Data.PNat.Xgcd

URI: https://scilib.ai/kg/mathlib#PNat.gcd_rel_right

English

For a,b ∈ ℕ+, we have (gcdW(a,b) · b) = (gcdY(a,b) · a) + gcd(a,b).

Русский

Для а,b ∈ ℕ+ выполняется (gcdW(a,b)·b) = (gcdY(a,b)·a) + gcd(a,b).

LaTeX

$$$\\gcdW(a,b) \\cdot b = \\gcdY(a,b) \\cdot a + \\gcd(a,b)$$$

Lean4

theorem gcd_rel_right : (gcdW a b * b : ℕ) = gcdY a b * a + gcd a b :=
  gcd_eq a b ▸ (gcd_props a b).2.2.2.2.2.2

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

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

Разделы

Аффилиация

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