R✝ : Type ?u.325967
R₁ : Type ?u.325970
R₂ : Type ?u.325973
R₃ : Type ?u.325976
k : Type ?u.325979
S : Type ?u.325982
S₃ : Type ?u.325985
T : Type ?u.325988
M✝ : Type ?u.325991
M₁ : Type ?u.325994
M₂ : Type ?u.325997
M₃ : Type ?u.326000
N₁ : Type ?u.326003
N₂ : Type ?u.326006
N₃ : Type ?u.326009
ι : Type ?u.326012
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R✝ M✝
inst✝³ : Module R✝ M₂
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
⊢ ∀ (c_1 : R) (x : M), c • c_1 • x = c_1 • c • x
R✝ : Type ?u.325967
R₁ : Type ?u.325970
R₂ : Type ?u.325973
R₃ : Type ?u.325976
k : Type ?u.325979
S : Type ?u.325982
S₃ : Type ?u.325985
T : Type ?u.325988
M✝ : Type ?u.325991
M₁ : Type ?u.325994
M₂ : Type ?u.325997
M₃ : Type ?u.326000
N₁ : Type ?u.326003
N₂ : Type ?u.326006
N₃ : Type ?u.326009
ι : Type ?u.326012
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R✝ M✝
inst✝³ : Module R✝ M₂
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
⊢ IsLinearMap R fun z => c • z
refine' IsLinearMap.mk (smul_add c) _
R✝ : Type ?u.325967
R₁ : Type ?u.325970
R₂ : Type ?u.325973
R₃ : Type ?u.325976
k : Type ?u.325979
S : Type ?u.325982
S₃ : Type ?u.325985
T : Type ?u.325988
M✝ : Type ?u.325991
M₁ : Type ?u.325994
M₂ : Type ?u.325997
M₃ : Type ?u.326000
N₁ : Type ?u.326003
N₂ : Type ?u.326006
N₃ : Type ?u.326009
ι : Type ?u.326012
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R✝ M✝
inst✝³ : Module R✝ M₂
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c c✝ : R
x✝ : M
⊢ c • c✝ • x✝ = c✝ • c • x✝
R✝ : Type ?u.325967
R₁ : Type ?u.325970
R₂ : Type ?u.325973
R₃ : Type ?u.325976
k : Type ?u.325979
S : Type ?u.325982
S₃ : Type ?u.325985
T : Type ?u.325988
M✝ : Type ?u.325991
M₁ : Type ?u.325994
M₂ : Type ?u.325997
M₃ : Type ?u.326000
N₁ : Type ?u.326003
N₂ : Type ?u.326006
N₃ : Type ?u.326009
ι : Type ?u.326012
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R✝ M✝
inst✝³ : Module R✝ M₂
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
⊢ ∀ (c_1 : R) (x : M), c • c_1 • x = c_1 • c • x
intro _ _
no goals
R✝ : Type ?u.325967
R₁ : Type ?u.325970
R₂ : Type ?u.325973
R₃ : Type ?u.325976
k : Type ?u.325979
S : Type ?u.325982
S₃ : Type ?u.325985
T : Type ?u.325988
M✝ : Type ?u.325991
M₁ : Type ?u.325994
M₂ : Type ?u.325997
M₃ : Type ?u.326000
N₁ : Type ?u.326003
N₂ : Type ?u.326006
N₃ : Type ?u.326009
ι : Type ?u.326012
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R✝ M✝
inst✝³ : Module R✝ M₂
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c c✝ : R
x✝ : M
⊢ c • c✝ • x✝ = c✝ • c • x✝
simp only [smul_smul, mul_comm]