cocycles₁_map_mul_of_isTrivial — Mathlib

English

If A is a trivial representation, then every 1‑cocycle f satisfies f(g h) = f(g) + f(h) for all g,h in G.

Русский

Если A тривиально как представление, то для любого 1‑кокцикла f имеем f(g h) = f(g) + f(h) для всех g,h ∈ G.

LaTeX

$$$\\\\forall f \\\\in cocycles_1(A), \\\\forall g,h \\\\in G \\\\quad f(g h) = f(g) + f(h).$$$

Lean4

theorem cocycles₁_map_mul_of_isTrivial [A.IsTrivial] (f : cocycles₁ A) (g h : G) : f (g * h) = f g + f h := by
  rw [(mem_cocycles₁_iff f).1 f.2, isTrivial_apply A.ρ g (f h), add_comm]

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