innerₛₗ_apply

Mathlib.Analysis.CStarAlgebra.Module.Defs

URI: https://scilib.ai/kg/mathlib#CStarModule.innerₛₗ_apply

English

The product carries a NormedAddCommGroup structure via a core construction.

Русский

Произведение имеет структуру нормированной аддитивной группы через ядро построения.

LaTeX

$$$\\mathrm{NormedAddCommGroup}(C\\,⋆ᵐᵒᵈ(A, Π_i E_i))$$$

Lean4

theorem innerₛₗ_apply {x y : E} : innerₛₗ x y = ⟪x, y⟫ :=
  rfl

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

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

Разделы

Аффилиация

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