coe_pow — Mathlib

English

The coercion-cast power correspondence: the nth power of an algebra equivalence corresponds to the nth iterate of its action on elements.

Русский

Соотношение степеней при приведении к функции: n-ая степень эквивалентности соответствует n-му повторному применению к элементам.

LaTeX

$$$ (e^{n}) = e^{[n]} $$$

Lean4

@[simp]
theorem coe_pow (e : A₁ ≃ₐ[R] A₁) (n : ℕ) : ⇑(e ^ n) = e^[n] :=
  n.rec (by ext; simp) fun _ ih ↦ by ext; simp [pow_succ, ih]

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