no goals
R : Type u_2
R₂ : Type ?u.274344
K : Type ?u.274347
M : Type u_1
M₂ : Type ?u.274353
V : Type ?u.274356
S : Type ?u.274359
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) = span R (↑(-LinearMap.id) '' s)
simp
no goals
R : Type u_2
R₂ : Type ?u.274344
K : Type ?u.274347
M : Type u_1
M₂ : Type ?u.274353
V : Type ?u.274356
S : Type ?u.274359
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ map (-LinearMap.id) (span R s) = span R s
simp