instStarId — Mathlib

English

The space of linear endomorphisms E → E forms a star algebra with the adjoint as the star operation.

Русский

Пространство концом линейных отображений E → E образует звёздную алгебру, где сопряжение задаётся как сопряжение по скалярному произведению.

LaTeX

$$$$\text{End}(E)\; \text{is a star algebra with } A^{*} = \text{adjoint}(A).$$$$

Lean4

/-- `E →ₗ[𝕜] E` is a star algebra with the adjoint as the star operation. -/
instance : Star (E →ₗ[𝕜] E) :=
  ⟨adjoint⟩

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