twoCochain_skew — Mathlib

English

Let a be a 2-cochain. Then for all x, y in the Lie algebra, its value is skew-symmetric: a(x, y) = -a(y, x). Equivalently, -a(x, y) = a(y, x).

Русский

Пусть a — двуцепочная; тогда она кососимметрична: для любых x, y в алгебре Ли имеет место a(x, y) = -a(y, x). Эквивалентно: -a(x, y) = a(y, x).

LaTeX

$$$-a(x,y) = a(y,x)\\quad(\\text{for all }x,y\\in L).$$$

Lean4

theorem twoCochain_skew (a : twoCochain R L M) (x y : L) : -a x y = a y x :=
  by
  rw [neg_eq_iff_add_eq_zero, add_comm]
  simpa [map_add, twoCochain_alt a x, twoCochain_alt a y] using twoCochain_alt a (x + y)

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