English
npowRec' is a variant of exponentiation that defines a map from natural numbers to the semigroup with base case 0 → 1, 1 → a, and for k+2 → npowRec'(k+1) · a.
Русский
npowRec' — это вариант возведения в степень: 0 → 1, 1 → a, а для k+2: npowRec'(k+1) · a.
LaTeX
$$$\\text{npowRec'}: \\mathbb{N} \\to M \\to M\\quad\\text{with}\\quad npowRec'(0, a)=1,\; npowRec'(1, a)=a,\; npowRec'(k+2, a)=npowRec'(k+1, a)\\cdot a.$$$
Lean4
/-- A variant of `npowRec` which is a semigroup homomorphism from `ℕ₊` to `M`.
-/
def npowRec' {M : Type*} [One M] [Mul M] : ℕ → M → M
| 0, _ => 1
| 1, m => m
| k + 2, m => npowRec' (k + 1) m * m
