innerSL_apply

Mathlib.Analysis.InnerProductSpace.LinearMap

URI: https://scilib.ai/kg/mathlib#innerSL_apply

English

One can form a linear isometry from a sesquilinear form by viewing it as a map into scalars.

Русский

Из билинейной/сесклярной формы можно построить линейную изометрию, рассматривая её как отображение в скаляры.

LaTeX

$$$ toSesqForm: E \\to E' \\Rightarrow \\text{isometry}$$$

Lean4

@[simp]
theorem innerSL_apply (v w : E) : innerSL 𝕜 v w = ⟪v, w⟫ :=
  rfl

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

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

Разделы

Аффилиация

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