ringEquiv_map_smul — Mathlib

English

The ring isomorphism ringEquiv intertwines smul: ringEquiv(r • x) = algebraMap_R_S r • ringEquiv(x).

Русский

Тождество кольцевого изоморота сохраняет умножение на скаляры: ringEquiv(r • x) = algebraMap_R_S r • ringEquiv(x).

LaTeX

$$$\mathrm{ringEquiv}_{R,S,A}(r \cdot x) = \bigl( \mathrm{algebraMap}_{R}^{S} r \bigr) \cdot \mathrm{ringEquiv}_{R,S,A}(x)$$$

Lean4

@[simp]
theorem ringEquiv_map_smul (r : R) (x : RestrictScalars R S A) :
    RestrictScalars.ringEquiv R S A (r • x) = algebraMap R S r • RestrictScalars.ringEquiv R S A x :=
  rfl

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