d₂₁_single_one_snd — Mathlib

English

If the second component is the identity, then d21 maps single(g,1) a to a pure copy of the action: single 1 (A.ρ g⁻¹ a).

Русский

Если вторая компонента равна единице, то d21 отображает single(g,1) a в единичный класс со значением A.ρ(g⁻¹)a.

LaTeX

$$$d_{21}A(\mathrm{single}(g,1)\otimes a) = \mathrm{single}(1)\big(A.\rho(g^{-1})a\big)$$$

Lean4

theorem d₂₁_single_one_snd (g : G) (a : A) : d₂₁ A (single (g, 1) a) = single 1 (A.ρ g⁻¹ a) := by simp [d₂₁]

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