mem_cocycles₂_iff — Mathlib

English

Equivalent form: f ∈ cocycles₂(A) iff f(g h, j) + f(g,h) = ρ_g(f(h,j)) + f(g,h j) for all g,h,j.

Русский

Эквивалентная форма: f ∈ cocycles₂(A) тогда и только тогда, когда для всех g,h,j выполняется f(gh,j) + f(g,h) = ρ_g(f(h,j)) + f(g,hj).

LaTeX

$$$$ f \\in cocycles_2(A) \\iff \\forall g,h,j \\in G, \\\\ f(gh,j) + f(g,h) = A.\\\\rho(g)(f(h,j)) + f(g,hj). $$$$

Lean4

theorem mem_cocycles₂_iff (f : G × G → A) :
    f ∈ cocycles₂ A ↔ ∀ g h j : G, f (g * h, j) + f (g, h) = A.ρ g (f (h, j)) + f (g, h * j) := by
  simp_rw [mem_cocycles₂_def, sub_eq_zero, sub_add_eq_add_sub, sub_eq_iff_eq_add, eq_comm, add_comm (f (_ * _, _))]

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