English
The two natural-power conventions npowRecAuto and npowBinRecAuto are equal as maps: npowRecAuto = npowBinRecAuto.
Русский
Две конвенции натуральной степени: npowRecAuto и npowBinRecAuto совпадают как отображения: npowRecAuto = npowBinRecAuto.
LaTeX
$$$\\text{npowRecAuto} = \\text{npowBinRecAuto}$$$
Lean4
/-- An abbreviation for `npowRec` with an additional typeclass assumption on associativity
so that we can use `@[csimp]` to replace it with an implementation by repeated squaring
in compiled code.
-/
@[to_additive /-- An abbreviation for `nsmulRec` with an additional typeclass assumptions on associativity
so that we can use `@[csimp]` to replace it with an implementation by repeated doubling in compiled
code as an automatic parameter. -/
]
abbrev npowRecAuto {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) : M :=
npowRec k m
