linearIsometryEquiv_coe_apply — Mathlib

English

For a unitary endomorphism u, the linear isometry equivalence associated to u coincides with the underlying linear map.

Русский

Для унитарного эндоморфизма u соответствующее линейное изометрическое эквивалентное отображение совпадает с базовым линейным отображением.

LaTeX

$$$linearIsometryEquiv(u) = u$ as maps$$

Lean4

@[simp]
theorem linearIsometryEquiv_coe_apply (u : unitary (H →L[𝕜] H)) : linearIsometryEquiv u = (u : H →L[𝕜] H) :=
  rfl

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