smul_convolution_eq_convolution_inv_mul

English

For finite A,B ⊆ G and s,x ∈ G, (s • A) convolved with B at x equals A convolved with (s⁻¹ • B) evaluated at x.

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp) vadd_addConvolution_eq_addConvolution_neg_add]
theorem smul_convolution_eq_convolution_inv_mul (A B : Finset G) (s x : G) :
    (s •> A).convolution B x = A.convolution B (s⁻¹ * x) :=
  by
  nth_rw 1 [← inv_inv x, ← inv_inv (s⁻¹ * x)]
  rw [← inv_inv B, ← card_smul_inter, ← card_smul_inter, mul_inv_rev, inv_inv, smul_smul]

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