coe_mk

Mathlib.Algebra.Module.LinearMap.Defs

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

English

The linear map obtained by mk has the same underlying function as f.

Русский

Линейное отображение, полученное через mk, имеет ту же базовую функцию, что и f.

LaTeX

$$$((\mathrm{LinearMap.mk} f h : M \to_\sigma M_3) : M \to M_3) = f$$$

Lean4

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

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

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

Разделы

Аффилиация

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