isMulCocycle₁_of_mem_cocycles₁

English

If f ∈ cocycles₁(Rep.ofMulDistribMulAction G M), then IsMulCocycle₁ f̄ where f̄ = Additive.toMul ∘ f.

Русский

Если f ∈ cocycles₁(Rep.ofMulDistribMulAction G M), то IsMulCocycle₁ f̄, где f̄ = Additive.toMul ∘ f.

LaTeX

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

Lean4

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

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