coe_linearMap_injective — Mathlib

English

The underlying linear map from BialgHom to linear maps is injective; the injection factors through CoalgHom and then to linear maps.

Русский

Подлежащее линейное отображение из BialgHom в линейные отображения инъективно; это отображение через CoalgHom и далее в линейные отображения сохраняет инъективность.

LaTeX

$$$\\mathrm{Injective}\\bigl((\\uparrow) : (A \\to_{R}^{\\!c} B) \\to (A \\to_{R}^{\\!L} B)\\bigr)$$$

Lean4

theorem coe_linearMap_injective : Function.Injective ((↑) : (A →ₐc[R] B) → A →ₗ[R] B) :=
  CoalgHom.coe_linearMap_injective.comp coe_coalgHom_injective

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