isMulCoboundary₁_of_mem_coboundaries₁

English

If f is in coboundaries₁, then Additive.ofMul ∘ f is a 1-coboundary.

Русский

Если f ∈ coboundaries₁, то Additive.ofMul ∘ f — 1-подобранная функция.

LaTeX

$$$f \\in coboundaries_1(Rep.ofMulDistribMulAction\\ G\\ M) \\Rightarrow IsMulCoboundary_1(\\text{Additive.ofMul} \\circ f)$$$

Lean4

theorem isMulCoboundary₁_of_mem_coboundaries₁ (f : G → M) (hf : f ∈ coboundaries₁ (Rep.ofMulDistribMulAction G M)) :
    IsMulCoboundary₁ (M := M) (Additive.ofMul ∘ f) :=
  by
  rcases hf with ⟨x, rfl⟩
  exact ⟨x, fun _ => rfl⟩

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