English
If ℂ-action associates with M-action on E, then the ℝ-action induced by ℂ via real restriction associates with the M-action on E, i.e., r • (m • e) = ( (r : ℂ) • m ) • e.
Русский
Если ℂ-действие ассоциируется с M-действием на E, то ℝ-действие, индуцированное ℂ через действительное ограничение, ассоциируется с M-действием на E: r • (m • e) = ((r : ℂ) • m) • e.
LaTeX
$$$ \forall r \in \mathbb{R}, \forall m \in M, \forall e \in E:\ r \cdot (m \cdot e) = ( (r : \mathbb{C}) \cdot m ) \cdot e. $$$
Lean4
/-- The scalar action of `ℝ` on a `ℂ`-module `E` induced by `Module.complexToReal` associates with
another scalar action of `M` on `E` whenever the action of `ℂ` associates with the action of `M`. -/
instance complexToReal {M E : Type*} [AddCommGroup M] [Module ℂ M] [AddCommGroup E] [Module ℂ E] [SMul M E]
[IsScalarTower ℂ M E] : IsScalarTower ℝ M E where
smul_assoc r _
_ :=
smul_assoc (r : ℂ) _
_
-- check that the following instance is implied by the one above.
