R : Type u_2
S : Type u_3
M : Type u_1
A : Type ?u.72538
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ ↑(AddEquiv.symm (addEquiv R S M)) (↑(algebraMap R S) r • s • x) = r • ↑(AddEquiv.symm (addEquiv R S M)) (s • x)
R : Type u_2
S : Type u_3
M : Type u_1
A : Type ?u.72538
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ ↑(AddEquiv.symm (addEquiv R S M)) ((r • s) • x) = r • ↑(AddEquiv.symm (addEquiv R S M)) (s • x)
rw [Algebra.smul_def, mul_smul]
no goals
R : Type u_2
S : Type u_3
M : Type u_1
A : Type ?u.72538
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ ↑(AddEquiv.symm (addEquiv R S M)) (↑(algebraMap R S) r • s • x) = r • ↑(AddEquiv.symm (addEquiv R S M)) (s • x)
rfl