Theorem: DividedPowerAlgebra.coe_dpScalarExtensionEquiv_symm (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).symm = ⇑(dpScalarExtensionInv R S M)
Tactic:
rfl
State after:
no goals