English
Let σ be a permutation of ι, and s a Finset of ι. If the moved elements lie in s, then rearranging the factors by σ does not change the product: ∏_{x∈s} f(σ x) = ∏_{x∈s} f x.
Русский
Пусть σ — перестановка множества ι, и s — Finset ι. Если переносимые элементы принадлежат s, то перестановка порядка множителей не изменяет произведение: ∏_{x∈s} f(σ x) = ∏_{x∈s} f x.
LaTeX
$$$\\forall \\sigma\\,\\forall s:\\mathrm{Finset}\\,\\iota,\\ \\prod x\\in s, f(\\sigma x) = \\prod x\\in s, f x$$$
Lean4
@[to_additive]
theorem _root_.Equiv.Perm.prod_comp (σ : Equiv.Perm ι) (s : Finset ι) (f : ι → M) (hs : {a | σ a ≠ a} ⊆ s) :
(∏ x ∈ s, f (σ x)) = ∏ x ∈ s, f x :=
by
convert (prod_map s σ.toEmbedding f).symm
exact (map_perm hs).symm
