antipode_single — Mathlib

English

In AddMonoidAlgebra, the antipode on a basis element single g a equals single (-g) (antipode a).

Русский

В AddMonoidAlgebra антипод на базисном элементе single g a равен single(-g) (antipode a).

LaTeX

$$@[simp] theorem antipode_single (g : G) (a : A) : antipode R (single g a) = single (-g) (antipode R a)$$

Lean4

@[simp]
theorem antipode_single (g : G) (a : A) : antipode R (single g a) = single (-g) (antipode R a) := by
  simp [AddMonoidAlgebra, antipode]

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