d₂₁_single_one_fst — Mathlib

English

When the first component equals the identity, the differential collapses to the unit contribution: d21 applied to single(1,g) a yields single 1 a.

Русский

Когда первая компонента равна единице, дифференциал сводится к единичному вкладу: d21( single(1,g) a ) = single 1 a.

LaTeX

$$$d_{21}A(\mathrm{single}(1,g)\otimes a) = \mathrm{single}(1)\otimes a$$$

Lean4

theorem d₂₁_single_one_fst (g : G) (a : A) : d₂₁ A (single (1, g) a) = single 1 a := by simp [d₂₁]

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