coe_linearMap_mk

Mathlib.RingTheory.Coalgebra.Hom

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

English

The underlying function of a nested coalgebra morphism built from f is f

Русский

Базовая функция построенного вложенного коалгоморфизма равна f

LaTeX

$$$$ ((\langle\langle\langle f, h_1 \rangle, h_2 \rangle, h_3, h_4 \rangle) : A \to B) = f $$$$

Lean4

@[simp, norm_cast]
theorem coe_linearMap_mk {f : A →ₗ[R] B} (h h₁) : ((⟨f, h, h₁⟩ : A →ₗc[R] B) : A →ₗ[R] B) = f :=
  rfl

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

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

Разделы

Аффилиация

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