instNormedAlgebraOfReal — Mathlib

English

For any R with a NormedField structure and a NormedAlgebra structure of R over Real, the complex numbers carry a NormedAlgebra structure over R obtained by restriction of scalars from ℂ to Real.

Русский

Для любой R с нормированным полем и NormedAlgebra-структурой R над Real комплексам добавляется структура NormedAlgebra над R, полученная ограничением скаляров с ℂ на Real.

LaTeX

$$$ \\text{NormedAlgebra }_{R} (\\mathbb{C}) $ (via restriction from \\mathbb{C} to \\mathbb{R})$$

Lean4

instance {R : Type*} [NormedField R] [NormedAlgebra R ℝ] : NormedAlgebra R ℂ where
  norm_smul_le r x := by rw [← algebraMap_smul ℝ r x, real_smul, norm_mul, norm_real, norm_algebraMap']

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