innerSL_apply

Mathlib.Analysis.CStarAlgebra.Module.Defs

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

English

The map innerSL coincides with the standard A-valued inner product: innerSL x y = ⟪x,y⟫_A.

Русский

Отображение innerSL совпадает с обычным вложенным произведением: innerSL x y = ⟪x,y⟫_A.

LaTeX

$$$\\text{innerSL}(x,y) = \\\\langle x, y \\\\rangle_A$$$

Lean4

theorem innerSL_apply {x y : E} : innerSL x y = ⟪x, y⟫_A :=
  rfl

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

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

Разделы

Аффилиация

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