lid_toCoalgEquiv — Mathlib

English

The left-identity map lid is equal to the coalgebra-level left-identity map on tensors.

Русский

Отображение левого идентификатора lid совпадает с коалгебрическим соответствием для левого тензорного произведения.

LaTeX

$$$\text{lid}_{R,B} = \text{Coalgebra.TensorProduct.lid} R B$$$

Lean4

@[simp]
theorem lid_toCoalgEquiv : (Bialgebra.TensorProduct.lid R B : R ⊗[R] B ≃ₗc[R] B) = Coalgebra.TensorProduct.lid R B :=
  rfl

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