fixedBy_subset_fixedBy_zpow — Mathlib

English

For any g ∈ G and integer j, the fixedBy set for g is contained in the fixedBy set for g^j: fixedBy α g ⊆ fixedBy α (g^j).

Русский

Для любого g ∈ G и целого j множество фиксированных точек g содержится во множестве фиксированных точек g^j.

LaTeX

$$$ fixedBy(α, g) \subseteq fixedBy(α, g^{j}) $$$

Lean4

@[to_additive]
theorem fixedBy_subset_fixedBy_zpow (g : G) (j : ℤ) : fixedBy α g ⊆ fixedBy α (g ^ j) := fun _ h ↦ mem_fixedBy_zpow h j

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