xgcd

Mathlib.Algebra.EuclideanDomain.Defs

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

← MathLib Explorer

English

xgcd x y equals the pair (gcdA x y, gcdB x y) by definition.

Русский

xgcd x y определяется как пара (gcdA x y, gcdB x y).

LaTeX

$$$$ \\text{For all } x,y:\\ xgcd(x,y) = (\\gcdA(x,y), \\gcdB(x,y)). $$$$

Lean4

/-- Use the extended GCD algorithm to generate the `a` and `b` values
  satisfying `gcd x y = x * a + y * b`. -/
def xgcd (x y : R) : R × R :=
  (xgcdAux x 1 0 y 0 1).2

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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