English
If the ℂ-action on E commutes with the M-action on E, then the induced ℝ-action on E via Module.complexToReal also commutes with the M-action on E.
Русский
Если ℂ-действие на E коммутирует с M-действием на E, то полученное через Module.complexToReal ℝ-действие на E также коммутирует с M-действием.
LaTeX
$$$ \forall r \in \mathbb{R}, \forall m \in M, \forall e \in E:\ r \cdot (m \cdot e) = m \cdot (r \cdot e) \quad(\text{где } r \cdot e := (r : \mathbb{C}) \cdot e). $$$
Lean4
/-- The scalar action of `ℝ` on a `ℂ`-module `E` induced by `Module.complexToReal` commutes with
another scalar action of `M` on `E` whenever the action of `ℂ` commutes with the action of `M`. -/
instance (priority := 900) complexToReal {M E : Type*} [AddCommGroup E] [Module ℂ E] [SMul M E] [SMulCommClass ℂ M E] :
SMulCommClass ℝ M E where smul_comm r _ _ := smul_comm (r : ℂ) _ _
