antipode_single — Mathlib

English

In the Hopf algebra structure on MonoidAlgebra, the antipode acts on a basis element by inverting the group element and applying antipode to the coefficient: antipode_R(single g a) = single g^{-1}(antipode_R a).

Русский

В структуре HopfAlgebra на MonoidAlgebra антипод действует на базисный элемент так: S(single g a) = single g^{-1}(S(a)).

LaTeX

$$$\text{antipode}\,R\,(\text{single } g\ a) = \text{single } g^{-1}(\text{antipode } R\ a).$$$

Lean4

@[simp]
theorem antipode_single (g : G) (a : A) : antipode R (single g a) = single g⁻¹ (antipode R a) := by
  simp [MonoidAlgebra, antipode]

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