d₃₂_single_one_thd — Mathlib

English

If the last component is the identity, d32 again yields a linear combination reflecting the action by ρ on the first two components.

Русский

Если последняя компонента единица, d32 снова даёт линейную комбинацию, отражающую действие ρ на первые две компоненты.

LaTeX

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

Lean4

theorem d₃₂_single_one_thd (g h : G) (a : A) :
    d₃₂ A (single (g, h, 1) a) = single (h, 1) (A.ρ g⁻¹ a) - single (g * h, 1) a := by simp [d₃₂]

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