one_trans

Mathlib.Analysis.Normed.Operator.LinearIsometry

URI: https://scilib.ai/kg/mathlib#LinearIsometryEquiv.one_trans

English

The left identity: 1.trans e equals e, i.e., id ∘ e = e.

Русский

Левая единица: 1.trans e = e, то есть id ∘ e = e.

LaTeX

$$$ 1 \circ e = e $$$

Lean4

@[simp]
theorem one_trans : (1 : E ≃ₗᵢ[R] E).trans e = e :=
  refl_trans _

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

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

Разделы

Аффилиация

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