addEquiv_symm_map_algebraMap_smul

English

The inverse addEquiv also respects the scalar action: (addEquiv)^{-1}( algebraMap_R^S r • x ) = r • (addEquiv)^{-1} x for r ∈ R, x ∈ M.

Русский

Обратная связка addEquiv сохраняет скалярное действие: (addEquiv)^{-1}( algebraMap_R^S r • x ) = r • (addEquiv)^{-1} x для r ∈ R, x ∈ M.

LaTeX

$$$(\mathrm{addEquiv}_{R,S,M})^{-1}( \mathrm{algebraMap}_{R}^S r \cdot x ) = r \cdot (\mathrm{addEquiv}_{R,S,M})^{-1} x$$$

Lean4

theorem addEquiv_symm_map_algebraMap_smul (r : R) (x : M) :
    (RestrictScalars.addEquiv R S M).symm (algebraMap R S r • x) = r • (RestrictScalars.addEquiv R S M).symm x :=
  rfl

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