English
The algebra structure on A over Real obtained by restricting scalars from ℂ to Real makes A a NormedAlgebra over Real when it is already a NormedAlgebra over ℂ.
Русский
Структура алгебры на A над Real, полученная ограничением скаляров ℂ → Real, превращает A в NormedAlgebra над Real, если A уже является NormedAlgebra над ℂ.
LaTeX
$$$ \\text{NormedAlgebra Real } A \\;\\Leftarrow\\; \\text{NormedAlgebra Complex } A $ (via restriction)$$
Lean4
/-- The algebra structure from `Algebra.complexToReal` is a normed algebra. -/
instance (priority := 900) _root_.NormedAlgebra.complexToReal {A : Type*} [SeminormedRing A] [NormedAlgebra ℂ A] :
NormedAlgebra ℝ A :=
NormedAlgebra.restrictScalars ℝ ℂ A
