lTensor_counit_comul — Mathlib

English

For any a in a coalgebra, applying the left tensor counit to the comultiplication yields a ⊗ 1.

Русский

Для любого a в коалгебре применение левого тензорного counit к копуляции даёт a ⊗ 1.

LaTeX

$$$\\mathrm{lTensor}_A(\\mathrm{counit})(\\mathrm{comul}(a)) = a \\otimes 1.$$$

Lean4

@[simp]
theorem lTensor_counit_comul (a : A) : counit.lTensor A (comul a) = a ⊗ₜ[R] 1 :=
  LinearMap.congr_fun lTensor_counit_comp_comul a

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