English
Abbreviation stating that npowBinRecAuto k m equals npowBinRec k m.
Русский
Сокращение: npowBinRecAuto k m = npowBinRec k m.
LaTeX
$$$\\forall k\\in\\mathbb{N},\\forall m:\\ npowBinRecAuto\\, k\\, m = npowBinRec\\, k\\, m$$$
Lean4
/-- An abbreviation for `npowBinRec` with an additional typeclass assumption on associativity
so that we can use it in `@[csimp]` for more performant code generation.
-/
@[to_additive /-- An abbreviation for `nsmulBinRec` with an additional typeclass assumption on associativity
so that we can use it in `@[csimp]` for more performant code generation
as an automatic parameter. -/
]
abbrev npowBinRecAuto {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) : M :=
npowBinRec k m
