IsMulCocycle₂ — Mathlib

English

A function f: G×G→M satisfies the multiplicative 2-cocycle condition if for all g,h,j ∈ G, f(gh,j) f(g,h) = g • f(h,j) f(g,hj).

Русский

Функция f: G×G→M удовлетворяет условию умноженного 2-коцикла: для всех g,h,j ∈ G выполняется f(gh,j) f(g,h) = g • f(h,j) f(g,hj).

LaTeX

$$$\forall g,h,j:\; f(gh,j) \cdot f(g,h) = g \cdot f(h,j) \cdot f(g,hj)$$$

Lean4

/-- A function `f : G × G → M` satisfies the multiplicative 2-cocycle condition if
`f(gh, j) * f(g, h) = g • f(h, j) * f(g, hj)` for all `g, h : G`. -/
def IsMulCocycle₂ (f : G × G → M) : Prop :=
  ∀ g h j : G, f (g * h, j) * f (g, h) = g • (f (h, j)) * f (g, h * j)

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