English
For every c in R and x in RestrictScalars R S M, the scalar action c • x is given by transporting the S-action via the addEquiv isomorphism: c • x = (addEquiv)^{-1}( algebraMap_R_S(c) • addEquiv(x) ).
Русский
Для каждого c ∈ R и x ∈ RestrictScalars R S M скалярное действие задаётся через изоморфизм addEquiv: c • x = (addEquiv)^{-1}( algebraMap_R_S(c) • addEquiv(x) ).
LaTeX
$$$ c \\cdot x = (\\mathrm{addEquiv}_{R,S,M})^{-1} \\bigl( (\\mathrm{algebraMap}_{R}^S c) \\cdot \\mathrm{addEquiv}_{R,S,M} x \\bigr) $$$
Lean4
theorem smul_def (c : R) (x : RestrictScalars R S M) :
c • x = (RestrictScalars.addEquiv R S M).symm (algebraMap R S c • RestrictScalars.addEquiv R S M x) :=
rfl