Theorems about the density of pointwise operations on finsets.

@[simp]

theorem Finset.dens_inv {α : Type u_1} [DecidableEq α] [InvolutiveInv α] [Fintype α] (s : Finset α) : s⁻¹.dens = s.dens

@[simp]

theorem Finset.dens_neg {α : Type u_1} [DecidableEq α] [InvolutiveNeg α] [Fintype α] (s : Finset α) : (-s).dens = s.dens

@[simp]

theorem Finset.dens_smul_finset {α : Type u_1} {β : Type u_2} [DecidableEq β] [Group α] [MulAction α β] [Fintype β] (a : α) (s : Finset β) : (a • s).dens = s.dens

@[simp]

theorem Finset.dens_vadd_finset {α : Type u_1} {β : Type u_2} [DecidableEq β] [AddGroup α] [AddAction α β] [Fintype β] (a : α) (s : Finset β) : (a +ᵥ s).dens = s.dens