gcd_det_eq

Mathlib.Data.PNat.Xgcd

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

English

The determinant-type identity holds: gcdW(a,b) * gcdZ(a,b) equals succPNat of gcdX(a,b) * gcdY(a,b).

Русский

Сохраняется идентичность типа детерминанта: gcdW(a,b) · gcdZ(a,b) = succPNat( gcdX(a,b) · gcdY(a,b) ).

LaTeX

$$$\gcdW(a,b) \cdot gcdZ(a,b) = \operatorname{succPNat}(gcdX(a,b) \cdot gcdY(a,b))$$$

Lean4

theorem gcd_det_eq : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b) :=
  (gcd_props a b).1

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

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

Разделы

Аффилиация

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