npowRec_eq — Mathlib

English

For a semigroup with identity, npowRec(k+1) m equals 1 · npowRec'(k+1) m.

Русский

Для полугруппы с единицей: npowRec(k+1) m = 1 · npowRec'(k+1) m.

LaTeX

$$$\\forall M\\,[One M]\\[Semigroup M],\\forall k\\in\\mathbb{N},\\forall m\\in M:\\ npowRec(k+1,m) = 1 \\cdot npowRec'(k+1,m)$$$

Lean4

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

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