id_coe

Mathlib.Algebra.Module.LinearMap.Defs

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

English

The underlying function of LinearMap.id equals the ordinary identity function.

Русский

Базовая функция LinearMap.id совпадает с обычной функцией идентичности.

LaTeX

$$$((\mathrm{LinearMap.id} : M \to_\ell[R] M) : M \to M) = \mathrm{id}$$$

Lean4

@[simp, norm_cast]
theorem id_coe : ((LinearMap.id : M →ₗ[R] M) : M → M) = _root_.id :=
  rfl

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

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

Разделы

Аффилиация

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