Theorem: DividedPowerAlgebra.coe_dpScalarExtensionEquiv (DividedPowers/DPAlgebra/BaseChange.lean)

State before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⇑(dpScalarExtensionEquiv R S M) = ⇑(dpScalarExtension R S M)
Tactic:
rfl
State after:
no goals