translate_iterate — Mathlib

English

Let f be a degree-one circle lift. For every real x and every natural n, the n-th iterate of the translation by x equals the translation by n x.

Русский

Пусть f — подъём степени единицы на Circle. Для любых x ∈ ℝ и любого натурального n н-ая итерация переноса на x равна переносу на n x.

LaTeX

$$$ \forall x \in \mathbb{R}, \forall n \in \mathbb{N}, \left(\mathrm{translate}(\mathrm{Multiplicative.ofAdd}(x))\right)^{[n]} = \mathrm{translate}(\mathrm{Multiplicative.ofAdd}(\uparrow n \cdot x)). $$$

Lean4

@[simp]
theorem translate_iterate (x : ℝ) (n : ℕ) :
    (translate (Multiplicative.ofAdd x))^[n] = translate (Multiplicative.ofAdd <| ↑n * x) := by
  rw [← coe_pow, ← Units.val_pow_eq_pow_val, translate_pow]

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