conjAut_pow — Mathlib

English

Let α: X ≅ Y and f ∈ Aut(X). For every n ∈ N, the conjugation by α sends f^n to (α.conjAut f)^n, i.e. α.conjAut(f^n) = (α.conjAut f)^n.

Русский

Пусть α: X ≅ Y и f ∈ Aut(X). Для любого n ∈ ℕ сопряжение α переводит f^n в (α.conjAut f)^n, то есть α.conjAut(f^n) = (α.conjAut f)^n.

LaTeX

$$$ \\alpha.\\mathrm{conjAut}(f^n) = (\\alpha.\\mathrm{conjAut} f)^n $$$

Lean4

@[simp]
theorem conjAut_pow (f : Aut X) (n : ℕ) : α.conjAut (f ^ n) = α.conjAut f ^ n :=
  map_pow α.conjAut f n

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