IsMulCoboundary₁ — Mathlib

English

If f is a 1-cocycle in the additive representation sense (i.e., f ∈ cocycles₁ of Rep.ofMulDistribMulAction G M), then Additive.ofMul ∘ f is a 1-cocycle.

Русский

Если f — 1-коцикл в аддитивном представлении, то Additive.ofMul ∘ f — 1-коцикл.

LaTeX

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

Lean4

/-- A function `f : G → M` satisfies the multiplicative 1-coboundary condition if there's `x : M`
such that `g • x / x = f(g)` for all `g : G`. -/
def IsMulCoboundary₁ (f : G → M) : Prop :=
  ∃ x : M, ∀ g : G, g • x / x = f g

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