English
Alternative Bezout coefficient function giving the second coefficient in the identity gcd x y = x·gcdA x y + y·gcdB x y.
Русский
Альтернативная функция коэффициента Безу, задающая второй коэффициент в тождестве gcd x y = x·gcdA x y + y·gcdB x y.
LaTeX
$$$$\\gcdB(x,y) : \\mathbb{Z} \\times \\mathbb{Z} \\to \\mathbb{Z},\\; \\text{such that } \\gcd(x,y) = x\\cdot\\gcdA(x,y) + y\\cdot\\gcdB(x,y).$$$$
Lean4
/-- The extended GCD `b` value in the equation `gcd x y = x * a + y * b`. -/
def gcdB : ℤ → ℤ → ℤ
| m, ofNat n => m.natAbs.gcdB n
| m, -[n+1] => -m.natAbs.gcdB n.succ
