coe_addHom_mk

Mathlib.Algebra.Module.LinearMap.Defs

URI: https://scilib.ai/kg/mathlib#LinearMap.coe_addHom_mk

English

The AddHom underlying the mk-construction equals f.

Русский

Базовая AddHom-структура, лежащая в основе mk, равна f.

LaTeX

$$$((LinearMap.mk f h : M \to_\sigma M_3) : AddHom M M_3) = f$$$

Lean4

@[simp]
theorem coe_addHom_mk {σ : R →+* S} (f : AddHom M M₃) (h) : ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : AddHom M M₃) = f :=
  rfl

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

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

Разделы

Аффилиация

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