F : Type ?u.942371
α : Type u_2
β : Type u_1
γ : Type ?u.942380
inst✝³ : Monoid α
inst✝² : AddGroup β
inst✝¹ : DistribMulAction α β
inst✝ : DecidableEq β
a : α
s : Finset α
t : Finset β
⊢ s • image (fun x => -x) t = image (fun x => -x) (s • t)
F : Type ?u.942371
α : Type u_2
β : Type u_1
γ : Type ?u.942380
inst✝³ : Monoid α
inst✝² : AddGroup β
inst✝¹ : DistribMulAction α β
inst✝ : DecidableEq β
a : α
s : Finset α
t : Finset β
⊢ s • -t = -(s • t)
simp_rw [← image_neg]
no goals
F : Type ?u.942371
α : Type u_2
β : Type u_1
γ : Type ?u.942380
inst✝³ : Monoid α
inst✝² : AddGroup β
inst✝¹ : DistribMulAction α β
inst✝ : DecidableEq β
a : α
s : Finset α
t : Finset β
⊢ s • image (fun x => -x) t = image (fun x => -x) (s • t)
exact image_image₂_right_comm smul_neg