English
The image of r under algebraMap R (RestrictScalars R S A) corresponds to the successive algebra maps R → S → A along the RestrictScalars construction: ringEquiv(algebraMap_R(RestrictScalars R S A) r) = algebraMap_S A (algebraMap R S r).
Русский
Образ элемента r под algebraMap R (RestrictScalars R S A) соответствует последовательному отображению алгебр R → S → A через RestrictScalars: ringEquiv(algebraMap_R(RestrictScalars R S A) r) = algebraMap_S A (algebraMap R S r).
LaTeX
$$$\mathrm{ringEquiv}_{R,S,A}(\mathrm{algebraMap}_{R}(\mathrm{RestrictScalars}(R,S,A)) r) = \mathrm{algebraMap}_{S}^{A}(\mathrm{algebraMap}_{R}^{S} r)$$$
Lean4
@[simp]
theorem ringEquiv_algebraMap (r : R) :
RestrictScalars.ringEquiv R S A (algebraMap R (RestrictScalars R S A) r) = algebraMap S A (algebraMap R S r) :=
rfl
