feat(Finset): (a • s).dens = s.dens (#17020)

From LeanAPAP

Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.BigOperators.Group.Finset
 import Mathlib.Algebra.Group.Action.Pi
 import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Algebra.Ring.Pointwise.Set
+import Mathlib.Data.Finset.Density
 import Mathlib.Data.Finset.NAry
 import Mathlib.Data.Set.Pointwise.Finite
 import Mathlib.Data.Set.Pointwise.ListOfFn
@@ -1697,6 +1698,9 @@ theorem smul_univ [Fintype β] {s : Finset α} (hs : s.Nonempty) : s • (univ :
 theorem card_smul_finset (a : α) (s : Finset β) : (a • s).card = s.card :=
   card_image_of_injective _ <| MulAction.injective _
 
+@[to_additive (attr := simp)]
+lemma dens_smul_finset [Fintype β] (a : α) (s : Finset β) : (a • s).dens = s.dens := by simp [dens]
+
 /-- If the left cosets of `t` by elements of `s` are disjoint (but not necessarily distinct!), then
 the size of `t` divides the size of `s • t`. -/
 @[to_additive "If the left cosets of `t` by elements of `s` are disjoint (but not necessarily