smul_fixedBy — Mathlib

English

For g, h ∈ G, the action of h on fixedBy g equals fixedBy of conjugated g: h • fixedBy g = fixedBy (h g h⁻¹).

Русский

Для элементов g, h ∈ G выполняется: h • fixedBy g = fixedBy (h g h⁻¹).

LaTeX

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

Lean4

@[to_additive]
theorem smul_fixedBy (g h : G) : h • fixedBy α g = fixedBy α (h * g * h⁻¹) :=
  by
  ext a
  simp_rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, mul_smul, smul_eq_iff_eq_inv_smul h]

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