convolution_inv — Mathlib

English

For A,B ⊆ G finite and x ∈ G, A * B(x⁻¹) = B⁻¹ * A⁻¹(x).

Русский

Для конечных A,B ⊆ G и x ∈ G выполняется A * B(x⁻¹) = B⁻¹ * A⁻¹(x).

LaTeX

$$$ (A * B)(x^{-1}) = (B^{-1} * A^{-1})(x) $$$

Lean4

@[to_additive (attr := simp) addConvolution_neg]
theorem convolution_inv (A B : Finset G) (x : G) : A.convolution B x⁻¹ = B⁻¹.convolution A⁻¹ x :=
  by
  nth_rw 1 [← inv_inv B]
  rw [← card_smul_inter, ← card_inter_smul, inter_comm]

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