smul_iterate — Mathlib

English

The n-th iterate of the smul by a equals the n-th power of a acting on the element: (a •)^[n] = a^n • (·).

Русский

n-е повторение действия смула на элементе равно действию a^n: (a •)^[n] = a^n • (·).

LaTeX

$$$\\\\forall a \\\\in M, \\\\forall n \\\\in \\mathbb{N}, \\\\ (a \\\\cdot ·)^[n] = (a^n \\\\cdot ·).$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_iterate (a : M) : ∀ n : ℕ, (a • · : α → α)^[n] = (a ^ n • ·)
  | 0 => by simp [funext_iff]
  | n + 1 => by ext; simp [smul_iterate, pow_succ, smul_smul]

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