one

Mathlib.Topology.Algebra.Module.LinearMap

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

English

The identity map corresponds to LinearMap.id under the coe to LinearMap.

Русский

Идентичное отображение соответствует LinearMap.id под переводом к линейному отображению.

LaTeX

$$$ (\text{ContinuousLinearMap.id } R_1 M_1 : M_1 \to\_{R_1} M_1)^{\toLinearMap} = \mathrm{LinearMap.id}. $$$

Lean4

instance one : One (M₁ →L[R₁] M₁) :=
  ⟨.id R₁ M₁⟩

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

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

Разделы

Аффилиация

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