fixedBy_inv — Mathlib

English

In a multiplicative group action, the set of points fixed by g⁻¹ is the same as those fixed by g: fixedBy α g⁻¹ = fixedBy α g.

Русский

При действии группы с умножением множества точек, фиксированных относительно g⁻¹, совпадают с фиксированными относительно g: fixedBy α g⁻¹ = fixedBy α g.

LaTeX

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

Lean4

/-- In a multiplicative group action, the points fixed by `g` are also fixed by `g⁻¹` -/
@[to_additive (attr := simp) /-- In an additive group action, the points fixed by `g` are also fixed by `g⁻¹` -/
    ]
theorem fixedBy_inv (g : G) : fixedBy α g⁻¹ = fixedBy α g :=
  by
  ext
  rw [mem_fixedBy, mem_fixedBy, inv_smul_eq_iff, eq_comm]

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