card_mul_inv_eq_convolution_inv — Mathlib

English

For A,B ⊆ G finite and x ∈ G, the number of pairs (a,b) ∈ A × B with a b⁻¹ = x equals (A * B⁻¹)(x).

Русский

Для конечных A,B ⊆ G и x ∈ G число пар (a,b) ∈ A × B с условием a b⁻¹ = x равно (A * B⁻¹)(x).

LaTeX

$$$ \#\{(a,b) \in A \times B : a b^{-1} = x\} = (A * B^{-1})(x) $$$

Lean4

@[to_additive card_add_neg_eq_addConvolution_neg]
theorem card_mul_inv_eq_convolution_inv (A B : Finset G) (x : G) :
    #({ab ∈ A ×ˢ B | ab.1 * ab.2⁻¹ = x}) = A.convolution B⁻¹ x :=
  card_nbij' (fun ab => (ab.1, ab.2⁻¹)) (fun ab => (ab.1, ab.2⁻¹)) (by simp [Set.MapsTo]) (by simp [Set.MapsTo])
    (by simp [Set.LeftInvOn]) (by simp [Set.LeftInvOn])

Похожие утверждения