single_mem_cycles₁_of_mem_invariants

English

If the representation A is trivial, then Z1(G,A) equals the whole domain G →₀ A (i.e. the top submodule).

Русский

Если представление A тривиально, то Z1(G,A) совпадает со всем пространством G →₀ A (верхний подмодуль).

LaTeX

$$Z_1(G,A) = ⊤ \text{ when } A \\text{ is trivial}$$

Lean4

theorem single_mem_cycles₁_of_mem_invariants (g : G) (a : A) (ha : a ∈ A.ρ.invariants) : single g a ∈ cycles₁ A :=
  (single_mem_cycles₁_iff g a).2 (ha g)

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