mem_cocycles₁_iff — Mathlib

English

A function f is a 1-cocycle if and only if for all g,h, f(gh) = ρ(g)(f(h)) + f(g).

Русский

Функция f является 1-циклом тогда и только тогда, когда для всех g,h выполняется f(gh) = ρ(g)(f(h)) + f(g).

LaTeX

$$$f ∈ cocycles_1 A ↔ ∀ g,h : G, f(gh) = A.ρ g (f h) + f g$$

Lean4

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

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