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

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : R
⊢ (algebraMapInv R M) ↑((⇑(proj' R M 0) ∘ ⇑(algebraMap R (DividedPowerAlgebra R M))) x) = x
Tactic:
rw [proj'_zero_comp_algebraMap]
State after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : R
⊢ (algebraMapInv R M) ((algebraMap R (DividedPowerAlgebra R M)) x) = x

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : R
⊢ (algebraMapInv R M) ((algebraMap R (DividedPowerAlgebra R M)) x) = x
Tactic:
exact algebraMap_leftInverse R M x
State after:
no goals