Theorem: DividedPowerAlgebra.mk_C (DividedPowers/DPAlgebra/Init.lean)

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ mk (C a) = (algebraMap R (DividedPowerAlgebra R M)) a
Tactic:
rw [← MvPolynomial.algebraMap_eq, AlgHom.commutes]
State after:
no goals