instNormProd — Mathlib

English

A C*-module structure on a product space is defined componentwise by the respective inner products on each factor.

Русский

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

LaTeX

$$$\\text{instCStarModuleProd}: CStarModule A (E \\times F) \\text{ defined by } \\langle (x_1,x_2),(y_1,y_2)\\rangle = \\langle x_1,y_1\\rangle + \\langle x_2,y_2\\rangle$$$

Lean4

noncomputable instance : Norm C⋆ᵐᵒᵈ(A, E × F) where norm x := √‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

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