English
For a semigroup with identity and distributivity of addition over multiplication, npowRec satisfies npowRec(m+n, a) = npowRec(m, a) · npowRec(n, a).
Русский
Для полугруппы с единицей и свойствами де́ления сложения над умножением npowRec удовлетворяет npowRec(m+n, a) = npowRec(m, a) · npowRec(n, a).
LaTeX
$$$\\forall M\\,[One M]\\,[Semigroup M]\\ (m,n:\\mathbb{N})\\ (n\\neq 0)\\ (a\\in M),\\ npowRec(m+n,a) = npowRec(m,a) \\cdot npowRec(n,a).$$$
Lean4
@[to_additive]
theorem npowRec_add : npowRec (m + n) a = npowRec m a * npowRec n a :=
by
obtain _ | n := n; · exact (hn rfl).elim
induction n with
| zero => simp only [npowRec, ha]
| succ n ih => rw [← Nat.add_assoc, npowRec, ih n.succ_ne_zero]; simp only [npowRec, mul_assoc]
