feat(Combinatorics/Additive): more convolution lemmas (leanprover-community#38795)

From AddCombi

Author: YaelDillies

Mathlib/Combinatorics/Additive/Convolution.lean

@@ -50,6 +50,19 @@ lemma card_inter_smul (A B : Finset G) (x : G) : #(A ∩ (x • B)) = A.convolut
 lemma card_smul_inter (A B : Finset G) (x : G) : #((x • A) ∩ B) = A.convolution B⁻¹ x⁻¹ := by
   simpa using card_smul_inter_smul _ _ x 1
 
+@[to_additive]
+lemma card_inter_smul_inv (A B : Finset G) (x : G) : #(A ∩ (x • B⁻¹)) = A.convolution B x := by
+  simp [card_inter_smul]
+
+@[to_additive]
+lemma card_mul_eq (A B : Finset G) (x : G) :
+    #{ab ∈ A ×ˢ B | ab.1 * ab.2 = x} = A.convolution B x := rfl
+
+@[to_additive]
+lemma card_div_eq (A B : Finset G) (x : G) :
+    #{ab ∈ A ×ˢ B | ab.1 / ab.2 = x} = A.convolution B⁻¹ x :=
+  Finset.card_equiv ((Equiv.refl _).prodCongr (.inv _)) (by simp [div_eq_mul_inv])
+
 @[to_additive card_add_neg_eq_addConvolution_neg]
 lemma card_mul_inv_eq_convolution_inv (A B : Finset G) (x : G) :
     #{ab ∈ A ×ˢ B | ab.1 * ab.2⁻¹ = x} = A.convolution B⁻¹ x :=
@@ -105,4 +118,14 @@ lemma convolution_op_smul_eq_convolution_mul_inv (A B : Finset G) (s x : G) :
   rw [← inv_inv (B <• s), inv_op_smul_finset_distrib, ← card_inter_smul, ← card_inter_smul,
     smul_smul]
 
+variable [Fintype G]
+
+@[to_additive (attr := simp) univ_addConvolution]
+lemma univ_convolution (B : Finset G) (a : G) : univ.convolution B a = #B := by
+  simp [← card_inter_smul_inv]
+
+@[to_additive (attr := simp) addConvolution_univ]
+lemma convolution_univ (A : Finset G) (a : G) : A.convolution univ a = #A := by
+  simp [← card_inter_smul_inv]
+
 end Finset