one_apply

Mathlib.Topology.Algebra.Module.LinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.one_apply

English

The identity map is equal to the standard id map: (1 : M1 →L[R1] M1) = .id R1 M1.

Русский

Идентичное отображение равно стандартному отображению: (1 : M1 →L[R1] M1) = .id R1 M1.

LaTeX

$$$ (1 : M_1 \to L[R_1] M_1) = \mathrm{.id} R_1 M_1. $$$

Lean4

@[simp]
theorem one_apply (x : M₁) : (1 : M₁ →L[R₁] M₁) x = x :=
  rfl

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

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

Разделы

Аффилиация

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