R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
⊢ ↑(cast R M (_ : 0 + 0 = 0)) (GradedMonoid.GMul.mul (↑algebraMap₀ r) (↑algebraMap₀ s)) = r • ↑algebraMap₀ s
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
⊢ ↑(cast R M (_ : 0 + 0 = 0)) (GradedMonoid.GMul.mul (↑algebraMap₀ r) (↑algebraMap₀ s)) = ↑algebraMap₀ (r * s)
rw [← smul_eq_mul, LinearEquiv.map_smul]
no goals
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
⊢ ↑(cast R M (_ : 0 + 0 = 0)) (GradedMonoid.GMul.mul (↑algebraMap₀ r) (↑algebraMap₀ s)) = r • ↑algebraMap₀ s
exact algebraMap₀_mul r (@algebraMap₀ R M _ _ _ s)