trans_toLinearEquiv — Mathlib

English

The coalgebra morphism underlying the transitive composition e1₂.trans e2₃ equals the composition of the respective coalgebra morphisms.

Русский

Композиция коалгоморфизмов, лежащая в основе траспозиции e1₂.trans e2₃, равна композиции соответствующих коалгоморфизмов.

LaTeX

$$$ (e_{12}.trans e_{23} : A \\to_{R}^{\\mathrm{coalg}} C) = e_{23}.\\mathrm{comp} (e_{12}) $$$

Lean4

theorem trans_toLinearEquiv : (e₁₂.trans e₂₃ : A ≃ₗ[R] C) = (e₁₂ : A ≃ₗ[R] B) ≪≫ₗ e₂₃ :=
  rfl

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