smul_def — Mathlib

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

Похожие утверждения