R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s' s : { x // x ∈ S }
m : M
⊢ s • s' • m = s' • s • m
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s' s : { x // x ∈ S }
m : M
⊢ 1 • s • s' • m = 1 • (s' * s) • m
simp only [mul_smul, one_smul]
no goals
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s' s : { x // x ∈ S }
m : M
⊢ s • s' • m = s' • s • m
rw [smul_comm]