gcd_rel_left

Mathlib.Data.PNat.Xgcd

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

English

For a,b ∈ ℕ+, we have (gcdZ(a,b) · a) = (gcdX(a,b) · b) + gcd(a,b).

Русский

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

LaTeX

$$$\\gcdZ(a,b) \\cdot a = \\gcdX(a,b) \\cdot b + \\gcd(a,b)$$$

Lean4

theorem gcd_rel_left : (gcdZ a b * a : ℕ) = gcdX a b * b + gcd a b :=
  gcd_eq a b ▸ (gcd_props a b).2.2.2.2.2.1

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

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

Разделы

Аффилиация

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