feat(algebra/pointwise): add preimage_smul and generalize a couple of…

… assumptions (#8600)

Some lemmas about smul spun off from #2819

src/algebra/pointwise.lean

@@ -539,14 +539,21 @@ lemma zero_smul_set [semiring α] [add_comm_monoid β] [module α β] {s : set 
   (0 : α) • s = (0 : set β) :=
 by simp only [← image_smul, image_eta, zero_smul, h.image_const, singleton_zero]
 
-lemma mem_inv_smul_set_iff [field α] [mul_action α β] {a : α} (ha : a ≠ 0) (A : set β) (x : β) :
-  x ∈ a⁻¹ • A ↔ a • x ∈ A :=
+lemma mem_inv_smul_set_iff [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) (A : set β)
+  (x : β) : x ∈ a⁻¹ • A ↔ a • x ∈ A :=
 by simp only [← image_smul, mem_image, inv_smul_eq_iff' ha, exists_eq_right]
 
-lemma mem_smul_set_iff_inv_smul_mem [field α] [mul_action α β] {a : α} (ha : a ≠ 0) (A : set β)
-  (x : β) : x ∈ a • A ↔ a⁻¹ • x ∈ A :=
+lemma mem_smul_set_iff_inv_smul_mem [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0)
+  (A : set β) (x : β) : x ∈ a • A ↔ a⁻¹ • x ∈ A :=
 by rw [← mem_inv_smul_set_iff $ inv_ne_zero ha, inv_inv']
 
+lemma preimage_smul [group α] [mul_action α β] (a : α) (t : set β) : (λ x, a • x) ⁻¹' t = a⁻¹ • t :=
+((mul_action.to_perm a).symm.image_eq_preimage _).symm
+
+lemma preimage_smul' [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) (t : set β) :
+  (λ x, a • x) ⁻¹' t = a⁻¹ • t :=
+preimage_smul (units.mk0 a ha) t
+
 end
 
 namespace finset