English
Let E be a additive group with a complex vector space structure. Then E carries a natural real vector space structure obtained by restricting scalars from C to R.
Русский
Пусть E — абелева группа, на ней задано структуру векторного пространства над ℂ. Тогда E естественным образом становится вещественным векторным пространством через ограничение скаляров с ℂ на ℝ.
LaTeX
$$$ (\forall E)\; (\\text{AddCommGroup}(E) \wedge \\text{Module}_{\\mathbb{C}}(E)) \Rightarrow \text{Module}_{\\mathbb{R}}(E) \text{ with } r \cdot e := (r : \\mathbb{C}) \cdot e. $$$
Lean4
instance (priority := 900) complexToReal (E : Type*) [AddCommGroup E] [Module ℂ E] : Module ℝ E :=
RestrictScalars.module ℝ ℂ E
