instNormedAddCommGroupProd

Mathlib.Analysis.CStarAlgebra.Module.Constructions

URI: https://scilib.ai/kg/mathlib#WithCStarModule.instNormedAddCommGroupProd

English

The norm on the product C⋆ᵐᵒᵈ(A, E×F) is given by the standard product norm.

Русский

Норма на произведении C*-модулей задаётся стандартной нормой произведения.

LaTeX

$$$\\|x\\| = \\sqrt{\\|x_1\\|^{2} + \\|x_2\\|^{2}}$$$

Lean4

noncomputable instance : NormedAddCommGroup C⋆ᵐᵒᵈ(A, E × F) :=
  .ofCoreReplaceAll (normedSpaceCore A) uniformity_prod_eq_aux isBounded_prod_iff_aux

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

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

Разделы

Аффилиация

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