prod_comp' — Mathlib

English

Variant of the previous result with a refined factor form: ∏_{x∈s} f(σ x) x = ∏_{x∈s} f x (σ^{-1} x).

Русский

Вариант предыдущего результата с более точной формой множителей: ∏_{x∈s} f(σ x) x = ∏_{x∈s} f x (σ^{-1} x).

LaTeX

$$$\\prod x \\in s, f(\\sigma x) \\; x = \\prod x \\in s, f x \\, (\\sigma^{-1} 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) = ∏ x ∈ s, f x (σ.symm x) :=
  by
  convert σ.prod_comp s (fun x => f x (σ.symm x)) hs
  rw [Equiv.symm_apply_apply]

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