adjoint_innerSL_apply — Mathlib

English

The adjoint of the operator sending x to ⟨x, •⟩ acts as expected on innerSL.

Русский

Сопряжённый оператор, задающий x ↦ ⟨x, •⟩, действует согласно ожиданиям на innerSL.

LaTeX

$$adjoint (innerSL 𝕜 x) = toSpanSingleton 𝕜 x$$

Lean4

theorem adjoint_innerSL_apply (x : E) : adjoint (innerSL 𝕜 x) = toSpanSingleton 𝕜 x :=
  ext_ring <| ext_inner_left 𝕜 <| fun _ => by simp [adjoint_inner_right]

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