complexToReal — Mathlib

English

The module structure from restricting scalars from ℂ to ℝ endows any NormedSpace E that is a NormedSpace over ℂ with a NormedSpace structure over ℝ.

Русский

Структура модуля, полученная путём ограничения скаляров ℂ → ℝ, наделяет любую нормированную пространство E (над ℂ) нормированным пространством над ℝ.

LaTeX

$$$ \\text{NormedSpace}_{\\mathbb{R}} E = \\text{NormedSpace complexToReal } E $$$

Lean4

/-- The module structure from `Module.complexToReal` is a normed space. -/
instance (priority := 900) _root_.NormedSpace.complexToReal : NormedSpace ℝ E :=
  NormedSpace.restrictScalars ℝ ℂ E

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