instNormedSpaceComplexForall — Mathlib

English

There is a NormedSpace structure on the product complex module for all i, i.e., C⋆ᵐᵒᵈ(A, Π_i E_i) is a NormedSpace over ℂ.

Русский

Существует структура NormedSpace на произведении комплексных модулей; C⋆ᵐᵒᵈ(A, Π_i E_i) — NormedSpace над ℂ.

LaTeX

$$$\\text{NormedSpace}_{\\mathbb{C}}\\bigl(C\\,⋆ᵐᵒᵈ(A, Π_i E_i)\\bigr)$$$

Lean4

noncomputable instance : NormedSpace ℂ C⋆ᵐᵒᵈ(A, Π i, E i) :=
  .ofCore (normedSpaceCore A)

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