xgcd_val

Mathlib.Data.Int.GCD

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

English

The XGCD of x and y is precisely the pair of Bézout coefficients, i.e. xgcd(x,y) = (gcdA(x,y), gcdB(x,y)).

Русский

Расширенный НОД 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) : xgcd x y = (gcdA x y, gcdB x y) := by unfold gcdA gcdB; constructor

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

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

Разделы

Аффилиация

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