toLinearMap_eq_coe

Mathlib.RingTheory.Coalgebra.Hom

URI: https://scilib.ai/kg/mathlib#CoalgHom.toLinearMap_eq_coe

English

The linear map underlying a coalgebra hom equals the coalgebra hom’s own linear map component

Русский

Линейное отображение, лежащее в основе коалгоморфизма, равно его линейному компоненту

LaTeX

$$$$ f^{\mathrm{toLinearMap}} = f $$$$

Lean4

@[simp]
theorem toLinearMap_eq_coe (f : A →ₗc[R] B) : f.toLinearMap = f :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru