R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ r • ↑(tprod R) isEmptyElim = r • GradedMonoid.GOne.one
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ ↑algebraMap₀ r = r • GradedMonoid.GOne.one
simp [algebraMap₀]
no goals
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ r • ↑(tprod R) isEmptyElim = r • GradedMonoid.GOne.one
congr