d₃₂_single — Mathlib

English

The action of d32 on a pure tensor single(g,a) is the alternating sum of four terms, each a single on a pair with A.ρ and multiplication.

Русский

Действие d32 на чистый тензор single(g,a) даёт чередующую сумму из четырех слагаемых, каждое из которых — единичное по паре с A.ρ и умножение.

LaTeX

$$$d_{32}A(\mathrm{single}(g,a)) = \mathrm{single}(g_2,g_3)(A.ρ(g_1^{-1})a) - \mathrm{single}(g_1g_2,g_3)a + \mathrm{single}(g_1,g_2g_3)a - \mathrm{single}(g_1,g_2)a$$$

Lean4

@[simp]
theorem d₃₂_single (g : G × G × G) (a : A) :
    d₃₂ A (single g a) =
      single (g.2.1, g.2.2) (A.ρ g.1⁻¹ a) - single (g.1 * g.2.1, g.2.2) a + single (g.1, g.2.1 * g.2.2) a -
        single (g.1, g.2.1) a :=
  by simp [d₃₂]

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