Assumptions:
TeX:
\operatorname{xgcd}\!\left(-1, b\right) = \left(1, -\left|\operatorname{sgn}\!\left(\left(b - 1\right) \left(b + 1\right)\right)\right|, \operatorname{sgn}\!\left(b\right) \left(\operatorname{sgn}\!\left(b + 1\right) - \operatorname{sgn}\!\left(b - 1\right)\right)\right)
b \in \mathbb{Z}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| XGCD | Extended greatest common divisor | |
| Abs | Absolute value | |
| Sign | Sign function | |
| ZZ | Integers |
Source code for this entry:
Entry(ID("1b47db"),
Formula(Equal(XGCD(-1, b), Tuple(1, Neg(Abs(Sign(Mul(Sub(b, 1), Add(b, 1))))), Mul(Sign(b), Sub(Sign(Add(b, 1)), Sign(Sub(b, 1))))))),
Variables(b),
Assumptions(Element(b, ZZ)))