npowRec'_mul_comm — Mathlib

English

For k ≠ 0 in a semigroup, m · npowRec'(k) m = npowRec'(k) m · m.

Русский

В полугруппе при k ≠ 0 выполняется: m · npowRec'(k) m = npowRec'(k) m · m.

LaTeX

$$$\\forall k,m:\\ k\\neq 0 \\Rightarrow m \\cdot npowRec'(k,m) = npowRec'(k,m) \\cdot m$$$

Lean4

@[to_additive]
theorem npowRec'_mul_comm {M : Type*} [Semigroup M] [One M] {k : ℕ} (k0 : k ≠ 0) (m : M) :
    m * npowRec' k m = npowRec' k m * m := by
  induction k using Nat.strongRecOn with
  | ind k' ih =>
    match k' with
    | 1 => simp [npowRec']
    | k + 2 => simp [npowRec', ← mul_assoc, ih]

Похожие утверждения