esymm_eq_sum_subtype — Mathlib

English

The nth elementary symmetric polynomial can be defined by summing over the subtype {s ⊆ σ | |s| = n}: esymm(σ,R,n) = ∑ t ∈ { s ⊆ σ | |s| = n }, ∏_{i∈t} X_i.

Русский

N-й элементарный симметрический полином определяется суммой по подтипу {s ⊆ σ | |s| = n}: esymm(σ,R,n) = ∑_{t} ∏_{i∈t} X_i.

LaTeX

$$$ esymm(\\sigma,R,n) = \\sum t : \\{ s : Finset(\\sigma) // |s| = n \\}, \\prod i \\in (t:Finset\\;\\sigma), X_i $$$

Lean4

/-- We can define `esymm σ R n` by summing over a subtype instead of over `powerset_len`. -/
theorem esymm_eq_sum_subtype (n : ℕ) : esymm σ R n = ∑ t : { s : Finset σ // #s = n }, ∏ i ∈ (t : Finset σ), X i :=
  sum_subtype _ (fun _ => mem_powersetCard_univ) _

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