mem_cocycles₁_of_addMonoidHom — Mathlib

English

If A is trivial and f is an additive monoid homomorphism from the additive group G to A, then f ∘ Additive.ofMul ∈ cocycles1(A).

Русский

Если A тривиально и f — гомоморфизм аддитивных моноидов от Additive G в A, то f ∘ Additive.ofMul принадлежит cocycles1(A).

LaTeX

$$$\\\\forall f \\\\in AddMonoidHom(\\\\text{Additive } G, A),\\\\; f \\\\circ Additive.ofMul \\\\in cocycles_1(A).$$$

Lean4

theorem mem_cocycles₁_of_addMonoidHom [A.IsTrivial] (f : Additive G →+ A) : f ∘ Additive.ofMul ∈ cocycles₁ A :=
  (mem_cocycles₁_iff _).2 fun g h => by
    simp only [Function.comp_apply, ofMul_mul, map_add, isTrivial_apply A.ρ g (f (Additive.ofMul h)),
      add_comm (f (Additive.ofMul g))]

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