op_smul_convolution_eq_convolution_smul

English

For A,B ⊆ G finite and s ∈ G, the smul of A by s on the left interacts with convolution by s: (A <• s) * B = A * (s • B).

Русский

Для конечных A,B ⊆ G и элемента s ∈ G скалярное умножение A слева на s и конвольвента взаимодействуют так: (A <• s) * B = A * (s • B).

LaTeX

$$$ (A^{<\!\bullet\!>} s) * B = A * (s \cdot B) $$$

Lean4

@[to_additive (attr := simp) op_vadd_addConvolution_eq_addConvolution_vadd]
theorem op_smul_convolution_eq_convolution_smul (A B : Finset G) (s : G) :
    (A <• s).convolution B = A.convolution (s • B) :=
  funext fun x =>
    by
    nth_rw 1 [← inv_inv B, ← inv_inv (s • B), inv_smul_finset_distrib s B, ← card_inter_smul, ← card_inter_smul,
      smul_comm]
    simp [← card_smul_finset (op s) (A ∩ _), smul_finset_inter]

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