mem_fixedBy_zpow — Mathlib

English

If a ∈ fixedBy α g, then for any integer j, a ∈ fixedBy α (g^j).

Русский

Если a ∈ fixedBy α g, то для любого целого j верно a ∈ fixedBy α (g^j).

LaTeX

$$$ a \in fixedBy(α, g) \Rightarrow a \in fixedBy(α, g^j) \text{ for all } j \in \mathbb{Z} $$$

Lean4

@[to_additive]
theorem mem_fixedBy_zpow {g : G} {a : α} (h : a ∈ fixedBy α g) (j : ℤ) : a ∈ fixedBy α (g ^ j) :=
  by
  rw [mem_fixedBy, zpow_smul_eq_iff_minimalPeriod_dvd, minimalPeriod_eq_one_iff_fixedBy.mpr h, Int.natCast_one]
  exact one_dvd j

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