cocyclesOfIsMulCocycle₁ — Mathlib

English

If f ∈ coboundaries₁(Rep.ofMulDistribMulAction G M), then Additive.ofMul ∘ f is a 1-coboundary.

Русский

Если f принадлежит coboundaries₁(Rep.ofMulDistribMulAction G M), то Additive.ofMul ∘ f является 1-подобранной функцией.

LaTeX

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

Lean4

/-- Given an abelian group `M` with a `MulDistribMulAction` of `G`, and a function
`f : G → M` satisfying the multiplicative 1-cocycle condition, produces a 1-cocycle for the
representation on `Additive M` induced by the `MulDistribMulAction`. -/
@[simps]
def cocyclesOfIsMulCocycle₁ {f : G → M} (hf : IsMulCocycle₁ f) : cocycles₁ (Rep.ofMulDistribMulAction G M) :=
  ⟨Additive.ofMul ∘ f, (mem_cocycles₁_iff (A := Rep.ofMulDistribMulAction G M) f).2 hf⟩

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