Trig polynomial degrees in Lean: a Submodule plus span_mul_span

To use 'degree of a trigonometric polynomial' in Mathlib without building a polynomial type, define trigPoly k : Submodule ℝ (ℝ → ℝ) := Submodule.span ℝ {g | ∃ n ≤ k, ∃ c, g = fun θ ↦ cos (n*θ + c)}. The phase c covers sin. Products: have := Submodule.mul_mem_mul hp hq; unfold trigPoly at this; rw [Submodule.span_mul_span] at this; refine Submodule.span_le.2 ?_ this; rintro _ ⟨g, ⟨m,hm,c,rfl⟩, h, ⟨n,hn,d,rfl⟩, rfl⟩. ((ℝ → ℝ) is an ℝ-algebra, so Submodule multiplication is available.) This leaves one identity, cos a cos b = ½cos(a+b) + ½cos(a-b), with a case split on n ≤ m for cos((m-n)θ + ...), using Nat.cast_sub and cos_neg. Orthogonality to all of trigPoly k is one induction hp using Submodule.span_induction (cases mem/zero/add/smul). Prove continuity of members first, also by span_induction, so the add case has integrability. I used this for Hurwitz's proof of Sturm–Hurwitz (≥ 2N sign changes): ∏ (cos d_j - cos(θ - m_j)) over pairs of cut points lies in trigPoly ⌊m/2⌋ by induction with Finset.prod_range_succ. The empty product needs (1 : ℝ → ℝ) = fun _ ↦ 1 proved by funext; simp, because exact fails on the unexposed Pi 1. Small gotchas: rw [Real.cos_sub] can hit the wrong cosine, so pass the arguments; linarith does not unfold set α := fun j ↦ θ (2j+1), so state the needed bounds as have h : α j ≤ θ m := ....