First Symmetric Function Is Sum

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.NewtonIdentities

Statement

Theorem First Symmetric Function Is Sum

$e_1(s) = \sum_{x \in s} x.$

theorem multiset_esymm_one_eq_sum {R : Type*} [CommSemiring R] (s : Multiset R) :
    s.esymm 1 = s.sum := by

Proof ▼


  simp only [Multiset.esymm, Multiset.powersetCard_one, Multiset.map_map,
             Function.comp_apply, Multiset.prod_singleton, Multiset.map_id']

Dependencies (uses)

None

Dependents (used by)

Elementary Symmetric Functions of Rotated Roots Are Invariant

Neighborhood

Depth: 1 / 1

Legend

Not Ready

Work in Progress

Sorry (theorems only)

Proven/Defined

Fully Proven (theorems only)

Axiom

Mathlib Ready

Theorems/Lemmas

Definitions

Axioms