gcd_a_eq

Mathlib.Data.PNat.Xgcd

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

English

a equals gcdA'(a,b) times gcd(a,b).

Русский

a равен gcdA'(a,b) умножить на gcd(a,b).

LaTeX

$$$a = gcdA'(a,b) \cdot gcd(a,b)$$$

Lean4

theorem gcd_a_eq : a = gcdA' a b * gcd a b :=
  gcd_eq a b ▸ (gcd_props a b).2.1

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

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

Разделы

Аффилиация

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