translate_pow — Mathlib

English

For x ∈ ℝ and n ∈ ℕ, translate by x to the n-th power equals translate by n x.

Русский

Для x ∈ ℝ и n ∈ ℕ трансляция на x в n-й степени равна трансляции на n x.

LaTeX

$$$\\forall x \\in \\mathbb{R},\\ \\forall n \\in \\mathbb{N},\\ translate(\\text{ofAdd }x)^{n} = translate(\\text{ofAdd }(n\\cdot x))$$$

Lean4

@[simp]
theorem translate_pow (x : ℝ) (n : ℕ) :
    translate (Multiplicative.ofAdd x) ^ n = translate (Multiplicative.ofAdd <| ↑n * x) :=
  translate_zpow x n

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