d₃₂_single_one_fst — Mathlib

English

If the first component is the identity, the differential reduces to a simple boundary: d32 at single(1,g,h) a equals single(1,gh) a − single(1,g) a.

Русский

Если первая компонента — единица, дифференциал сводится к простому границе: d32( single(1,g,h) a ) = single(1,gh) a − single(1,g) a.

LaTeX

$$$d_{32}A(\mathrm{single}(1,g,h)\otimes a) = \mathrm{single}(1,gh)\otimes a - \mathrm{single}(1,g)\otimes a$$$

Lean4

theorem d₃₂_single_one_fst (g h : G) (a : A) : d₃₂ A (single (1, g, h) a) = single (1, g * h) a - single (1, g) a := by
  simp [d₃₂]

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