no goals
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : SMul R M
inst✝¹ : MulAction A M
inst✝ : IsScalarTower R A M
r : R
x : M
⊢ ↑(algebraMap R A) r • x = r • x
rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]