addEquiv_map_smul — Mathlib

English

The intertwining isomorphism addEquiv commutes with the R-action: for all c ∈ R and x ∈ RestrictScalars R S M, addEquiv(c • x) = algebraMap_R^S(c) • addEquiv(x).

Русский

Привязка addEquiv сохраняет скалярное действие: для всех c ∈ R и x ∈ RestrictScalars R S M верно addEquiv(c • x) = algebraMap_R^S(c) • addEquiv(x).

LaTeX

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

Lean4

@[simp]
theorem addEquiv_map_smul (c : R) (x : RestrictScalars R S M) :
    RestrictScalars.addEquiv R S M (c • x) = algebraMap R S c • RestrictScalars.addEquiv R S M x :=
  rfl

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