sum_mul_antipode_eq_smul — Mathlib

English

Similarly, the sum over i of left i times antipode(right i) equals counit(a) times 1.

Русский

Аналогично, сумма по i от left i умноженного на antipode(right i) равна counit(a) умноженное на 1.

LaTeX

$$$\sum_{i \in \text{repr.index}} \bigl( \text{repr.left } i \bigr) \cdot antipode\,R\,(\text{repr.right } i) = \mathrm{counit}\,(R\,a) \cdot 1$$$

Lean4

theorem sum_mul_antipode_eq_smul (repr : Repr R a) :
    ∑ i ∈ repr.index, repr.left i * antipode R (repr.right i) = counit (R := R) a • 1 := by
  rw [sum_mul_antipode_eq_algebraMap_counit, Algebra.smul_def, mul_one]

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