conjAut_zpow — Mathlib

English

Let α: X ≅ Y and f ∈ Aut(X). For any n ∈ Z, the conjugation by α preserves integer powers: α.conjAut (f^n) = (α.conjAut f)^n.

Русский

Пусть α: X ≅ Y и f ∈ Aut(X). Для любого n ∈ ℤ сопряжение α сохраняет целочисленные степени: α.conjAut(f^n) = (α.conjAut f)^n.

LaTeX

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

Lean4

@[simp]
theorem conjAut_zpow (f : Aut X) (n : ℤ) : α.conjAut (f ^ n) = α.conjAut f ^ n :=
  map_zpow α.conjAut f n

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