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

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Function.Surjective ⇑mk
Tactic:
apply RingQuot.mkAlgHom_surjective
State after:
no goals