List Foldr Equals Multiset Product

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.TrigonometricIdentities

Statement

Theorem List Foldr Equals Multiset Product
[blueprint]

For a list $l$ of real roots, $\mathrm{foldr}\bigl((r, p) \mapsto (X - C\,r) \cdot p,\; 1,\; l\bigr) = \prod_{r \in l} (X - C\,r).$

theorem list_foldr_eq_multiset_prod (l : List ℝ) :
    List.foldr (fun r p => (X - C r) * p) 1 l =
    (Multiset.map (fun r => X - C r) (l : Multiset ℝ)).prod := by
Proof ▼ 


  induction l with
  | nil =>
    simp [Multiset.map_zero]
  | cons head tail ih =>
    simp only [List.foldr]
    have h_coe : ((head :: tail) : Multiset ℝ) = head ::ₘ (tail : Multiset ℝ) := rfl
    rw [h_coe]
    simp only [Multiset.map_cons, Multiset.prod_cons]
    rw [ih]

Dependencies (uses)

None

Dependents (used by)

Neighborhood

Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms