English
npowBinRec defines exponentiation by repeated squaring for a semigroup with identity; it is implemented by a tail-recursive go function that composes multiplications according to the binary expansion of the exponent.
Русский
npowBinRec задаёт возведение в степень бинарным методом повторного возведения в квадрат в полугруппе с единицей; реализован через хвостовую рекурсию go, которая перемножает в соответствии с двоичным разложением степени.
LaTeX
$$$\\text{npowBinRec}$ is the efficient exponentiation by repeated squaring in a semigroup with identity; the auxiliary function $\\text{go}$ implements the binary Recursor to accumulate powers according to the bits of the exponent.$$
Lean4
/-- Exponentiation by repeated squaring. -/
@[to_additive /-- Scalar multiplication by repeated self-addition,
the additive version of exponentiation by repeated squaring. -/
]
def npowBinRec {M : Type*} [One M] [Mul M] (k : ℕ) : M → M :=
npowBinRec.go k 1
where/-- Auxiliary tail-recursive implementation for `npowBinRec`. -/
@[to_additive nsmulBinRec.go /-- Auxiliary tail-recursive implementation for `nsmulBinRec`. -/
]
go (k : ℕ) : M → M → M := k.binaryRec (fun y _ ↦ y) fun bn _n fn y x ↦ fn (cond bn (y * x) y) (x * x)
