op_smul_finset_mul_eq_mul_smul_finset

English

For any a in the semigroup and Finsets s, t, the identity op(a) • s * t = s * a • t holds, expressing a distribution of the action across a product.

Русский

Для любого элемента a полугруппы и Finset-ов s, t выполняется равенство op(a) • s * t = s * a • t, что выражает распределение действия над произведением.

LaTeX

$$$ (\\operatorname{op}(a) \\cdot s) \\cdot t = s \\cdot (a \\cdot t) $$$

Lean4

@[to_additive]
theorem op_smul_finset_mul_eq_mul_smul_finset (a : α) (s : Finset α) (t : Finset α) : op a • s * t = s * a • t :=
  op_smul_finset_smul_eq_smul_smul_finset _ _ _ fun _ _ _ => mul_assoc _ _ _

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