Theorem: DividedPowerAlgebra.coeff_exp_LinearMap (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
n : ℕ
m : M
⊢ (coeff (DividedPowerAlgebra R M) n) ↑((exp_LinearMap R M) m) = dp R n m
Tactic:
rw [coe_exp_LinearMap, coeff_exp]
State after:
no goals