mem_fixedBy_zpowers_iff_mem_fixedBy

English

For a ∈ α and g ∈ G, a is fixed by all g^j for all integers j if and only if a is fixed by g.

Русский

Для a ∈ α и g ∈ G верно: ∀ j ∈ ℤ, a фиксируется g^j тогда и только тогда, когда a фиксируется g.

LaTeX

$$$ (\forall j : \mathbb{Z}, a \in fixedBy(α, g^{j})) \Leftrightarrow a \in fixedBy(α, g) $$$

Lean4

@[to_additive]
theorem mem_fixedBy_zpowers_iff_mem_fixedBy {g : G} {a : α} : (∀ j : ℤ, a ∈ fixedBy α (g ^ j)) ↔ a ∈ fixedBy α g :=
  ⟨fun h ↦ by simpa using h 1, fun h j ↦ mem_fixedBy_zpow h j⟩

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