coalgebra_rid_eq_algebra_rid_apply

English

The right-identity rid equals the coalgebra-level right-identity equvialence.

Русский

Правый идентификатор rid равен коалгебра-эквивалентности правого идентификатора.

LaTeX

$$$\text{rid}_{R,B} : A ⊗[R] R \to_{bialg} A = \text{Coalgebra.TensorProduct.rid } R S A$$$

Lean4

theorem coalgebra_rid_eq_algebra_rid_apply (x : A ⊗[R] R) :
    Coalgebra.TensorProduct.rid R S A x = Algebra.TensorProduct.rid R R A x :=
  rfl

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