Theorem: DividedPowerAlgebra.coeff_exp (DividedPowers/DPAlgebra/Exponential.lean)

State before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
n : ℕ
⊢ (coeff (DividedPowerAlgebra R M) n) ↑(exp R m) = dp R n m
Tactic:
simp only [coe_exp, coeff_exp']
State after:
no goals