English
For finite A,B ⊆ G and elements x,y ∈ G, the size of the intersection (x • A) ∩ (y • B) equals the convolution of A with B⁻¹ evaluated at x⁻¹ y.
Русский
Для конечных A,B ⊆ G и элементов x,y ∈ G размер пересечения (x • A) ∩ (y • B) равен сверткe A * B⁻¹ в точке x⁻¹ y.
LaTeX
$$$ \big|(x \cdot A) \cap (y \cdot B)\big| = (A * B^{-1})(x^{-1} y) $$$
Lean4
@[to_additive]
theorem card_smul_inter_smul (A B : Finset G) (x y : G) : #((x • A) ∩ (y • B)) = A.convolution B⁻¹ (x⁻¹ * y) :=
card_nbij' (fun z ↦ (x⁻¹ * z, z⁻¹ * y)) (fun ab' ↦ x • ab'.1)
(by simp +contextual [Set.MapsTo, Set.mem_smul_set_iff_inv_smul_mem, mul_assoc])
(by
simp +contextual [Set.MapsTo, Set.mem_smul_set_iff_inv_smul_mem]
simp +contextual [← eq_mul_inv_iff_mul_eq, mul_assoc])
(by simp [Set.LeftInvOn]) (by simp +contextual [Set.LeftInvOn, ← eq_mul_inv_iff_mul_eq, mul_assoc])
