toSesqForm_apply_coe

Mathlib.Analysis.InnerProductSpace.LinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.toSesqForm_apply_coe

English

The real version of innerSLFlip coincides with real inner product symmetry.

Русский

В вещественном случае innerSLFlip совпадает с симметрией вещественного скалярного произведения.

LaTeX

$$$ (innerSLFlip \\ 𝕜).real = real\\_inner\\_comm $$$

Lean4

@[simp]
theorem toSesqForm_apply_coe (f : E →L[𝕜] E') (x : E') : toSesqForm f x = (innerSL 𝕜 x).comp f :=
  rfl

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

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

Разделы

Аффилиация

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