smul_inv_mem_fixedBy_iff_mem_fixedBy

English

For a ∈ α and g ∈ G, g⁻¹ • a ∈ fixedBy α g if and only if a ∈ fixedBy α g.

Русский

Для a ∈ α и g ∈ G, g⁻¹ • a ∈ fixedBy α g тогда и только тогда, когда a ∈ fixedBy α g.

LaTeX

$$$ g^{-1} \cdot a \in fixedBy(α, g) \iff a \in fixedBy(α, g) $$$

Lean4

@[to_additive]
theorem smul_inv_mem_fixedBy_iff_mem_fixedBy {a : α} {g : G} : g⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g := by
  rw [← fixedBy_inv, smul_mem_fixedBy_iff_mem_fixedBy, fixedBy_inv]

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