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

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ dp R 0 m = 1
Tactic:
rw [dp_def, ← map_one (mkAlgHom R (Rel R M))]
State after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (mkAlgHom R (Rel R M)) (X (0, m)) = (mkAlgHom R (Rel R M)) 1

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (mkAlgHom R (Rel R M)) (X (0, m)) = (mkAlgHom R (Rel R M)) 1
Tactic:
exact RingQuot.mkAlgHom_rel R Rel.zero
State after:
no goals