smul_zpow_fixedBy_eq_of_commute — Mathlib

English

If g and h commute, then h^j • fixedBy α g = fixedBy α g for all j ∈ ℤ.

Русский

Если g и h коммутируют, то h^j • fixedBy α g = fixedBy α g для всех j ∈ ℤ.

LaTeX

$$$ h^{j} \cdot fixedBy(α, g) = fixedBy(α, g) $$$

Lean4

/-- If `g` and `h` commute, then `g` fixes `(h ^ j) • x` iff `g` fixes `x`.
-/
@[to_additive /-- If `g` and `h` commute, then `g` fixes `(j • h) +ᵥ x` iff `g` fixes `x`. -/
    ]
theorem smul_zpow_fixedBy_eq_of_commute {g h : G} (comm : Commute g h) (j : ℤ) : h ^ j • fixedBy α g = fixedBy α g :=
  fixedBy_subset_fixedBy_zpow (Set α) h j (fixedBy_mem_fixedBy_of_commute comm)

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