isMulCocycle₂_of_mem_cocycles₂

English

If f ∈ coboundaries₂(Rep.ofMulDistribMulAction G M), then Additive.toMul ∘ f is a 2-coboundary.

Русский

Если f ∈ coboundaries₂(Rep.ofMulDistribMulAction G M), то Additive.toMul ∘ f — 2-подобранная функция.

LaTeX

$$$f \\in coboundaries_2(Rep.ofMulDistribMulAction\\ G\\ M) \\Rightarrow IsMulCoboundary_2(\\text{Additive.toMul} \\circ f)$$$

Lean4

theorem isMulCocycle₂_of_mem_cocycles₂ (f : G × G → M) (hf : f ∈ cocycles₂ (Rep.ofMulDistribMulAction G M)) :
    IsMulCocycle₂ (Additive.toMul ∘ f) :=
  (mem_cocycles₂_iff (A := Rep.ofMulDistribMulAction G M) f).1 hf

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