xgcd_val

Mathlib.Algebra.EuclideanDomain.Defs

URI: https://scilib.ai/kg/mathlib#EuclideanDomain.xgcd_val

English

The value of xgcd(x,y) is the pair (gcdA x y, gcdB x y).

Русский

Значение xgcd(x,y) равно паре (gcdA x y, gcdB x y).

LaTeX

$$$$ xgcd(x,y) = (\\gcdA(x,y), \\gcdB(x,y)). $$$$

Lean4

theorem xgcd_val (x y : R) : xgcd x y = (gcdA x y, gcdB x y) :=
  rfl

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

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

Разделы

Аффилиация

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