twoCochain_alt

Mathlib.Algebra.Lie.Cochain

URI: https://scilib.ai/kg/mathlib#LieModule.Cohomology.twoCochain_alt

English

For any a ∈ twoCochain R L M and any x ∈ L, a x x = 0.

Русский

Для любого a ∈ twoCochain R L M и любого x ∈ L выполняется a x x = 0.

LaTeX

$$$ a(x)(x) = 0, \quad \text{for all } a \in twoCochain(R,L,M), x \in L. $$$

Lean4

@[simp]
theorem twoCochain_alt (a : twoCochain R L M) (x : L) : a x x = 0 :=
  a.2 x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru