convolution_op_smul_eq_convolution_mul_inv

English

For A,B ⊆ G finite and s ∈ G, the convolution with B on the right and smul on B equals convolution with B and smul on A in a dual sense: A.convolution (B <• s) x = A.convolution B (x * s⁻¹).

Русский

Для конечных A,B ⊆ G и s ∈ G существует тождество: A.convolution (B <• s) x = A.convolution B (x s⁻¹).

LaTeX

$$$ A * (B <• s) (x) = A * B (x \, s^{-1}) $$$

Lean4

@[to_additive (attr := simp) addConvolution_op_vadd_eq_addConvolution_add_neg]
theorem convolution_op_smul_eq_convolution_mul_inv (A B : Finset G) (s x : G) :
    A.convolution (B <• s) x = A.convolution B (x * s⁻¹) :=
  by
  nth_rw 2 [← inv_inv B]
  rw [← inv_inv (B <• s), inv_op_smul_finset_distrib, ← card_inter_smul, ← card_inter_smul, smul_smul]

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