star_eq_symm — Mathlib

English

For a linear isometry e: H ≃ₗᵢ[𝕜] H, the star (the involution on endomorphisms) of the associated map equals its inverse. Concretely, star(e) = e^{-1}.

Русский

Для линейной изометрии e: H ≃ₗᵢ[𝕜] H звёздочка (инволюция на операторах) применительно к соответствующему отображению даёт обратное: e^{*} = e^{-1}.

LaTeX

$$$\star\bigl(e: H \to_L[𝕜] H\bigr) = e^{-1}$$$

Lean4

@[simp]
theorem _root_.LinearIsometryEquiv.star_eq_symm (e : H ≃ₗᵢ[𝕜] H) : star (e : H →L[𝕜] H) = e.symm :=
  e.adjoint_eq_symm

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