Theorem: DividedPowerAlgebra.algebraMap_leftInverse (DividedPowers/DPAlgebra/Graded/GradeZero.lean)

State before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
m : R
⊢ (algebraMapInv R M) ((algebraMap R (DividedPowerAlgebra R M)) m) = m
Tactic:
simp only [AlgHom.commutes, Algebra.id.map_eq_id, RingHom.id_apply]
State after:
no goals