d₂₁_single_self_inv_ρ_sub_inv_self

English

A symmetric variant of the previous relation where one subtracts the swapped single terms, yielding a difference of unit contributions tied to the action by ρ(g).

Русский

Симметричный вариант предыдущего соотношения, в котором вычитаются поменянные члены, давая разность единичных вкладов, связанная с действием ρ(g).

LaTeX

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

Lean4

theorem d₂₁_single_self_inv_ρ_sub_inv_self (g : G) (a : A) :
    d₂₁ A (single (g, g⁻¹) (A.ρ g a) - single (g⁻¹, g) a) = single 1 a - single 1 (A.ρ g a) :=
  by
  simp only [map_sub, d₂₁_single (G := G), inv_self_apply, mul_inv_cancel, inv_inv, inv_mul_cancel]
  abel

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