mem_invariants_iff_of_forall_mem_zpowers

English

For a group element g, if every x ∈ ⟨g⟩^⊤ (z-powers) lies in a subgroup, then v ∈ invariants iff ρ(g) v = v.

Русский

Для элемента g группы, если все x в zpowers лежат в подгруппе, то v ∈ инвариантов тогда и только тогда ρ(g) v = v.

LaTeX

$$$$ v \in \rho.invariants \iff \rho(g) v = v. $$$$

Lean4

theorem mem_invariants_iff_of_forall_mem_zpowers (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) (x : V) :
    x ∈ ρ.invariants ↔ ρ g x = x :=
  ⟨fun h => h g, fun hx γ => by
    rcases hg γ with ⟨i, rfl⟩
    induction i with
    | zero => simp
    | succ i _ => simp_all [zpow_add_one]
    | pred i h => _
    simpa [neg_sub_comm _ (1 : ℤ), zpow_sub] using congr(ρ g⁻¹ $(h.trans hx.symm))⟩

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