trans_one

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

The right identity for composition: e.trans 1 equals e, i.e., e ∘ id = e.

Русский

Правая единица для композиции: e.trans 1 = e, то есть e ∘ id = e.

LaTeX

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

Lean4

@[simp]
theorem trans_one : e.trans (1 : E₂ ≃ₗᵢ[R₂] E₂) = e :=
  trans_refl _

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

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

Разделы

Аффилиация

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