nsmulRec' — Mathlib

English

nsmulRec' is a variant of the additive power map, defined by 0 → 0, 1 → a, and for k+2 → nsmulRec'(k+1) + a.

Русский

nsmulRec' — вариант отображения кратности сложением: 0 → 0, 1 → a, а для k+2: nsmulRec'(k+1) + a.

LaTeX

$$$\\text{nsmulRec'}: \\mathbb{N} \\to M \\to M\\quad\\text{with}\\quad nsmulRec'(0,x)=0,\; nsmulRec'(1,x)=x,\; nsmulRec'(k+2,x)=nsmulRec'(k+1,x)+x.$$$

Lean4

/-- A variant of `nsmulRec` which is a semigroup homomorphism from `ℕ₊` to `M`.
-/
def nsmulRec' {M : Type*} [Zero M] [Add M] : ℕ → M → M
  | 0, _ => 0
  | 1, m => m
  | k + 2, m => nsmulRec' (k + 1) m + m

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