doc(Chebyshev): update TODO (#34037)

RootsExtrema fulfills one TODO and is the appropriate place for another.

Author: YuvalFilmus

Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean

@@ -22,6 +22,10 @@ import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
 * T_n(x) ∈ [-1, 1] iff x ∈ [-1, 1]: `abs_eval_T_real_le_one_iff`
 * Zeroes of T and U: `roots_T_real`, `roots_U_real`
 * Local extrema of T: `isLocalExtr_T_real_iff`, `isExtrOn_T_real_iff`
+
+## TODO
+
+Prove that the roots of the Chebyshev polynomials (except 0) are irrational.
 -/
 
 public section

Mathlib/RingTheory/Polynomial/Chebyshev.lean

@@ -54,8 +54,6 @@ and do not have `map (Int.castRingHom R)` interfering all the time.
 
 * Redefine and/or relate the definition of Chebyshev polynomials to `LinearRecurrence`.
 * Add explicit formula involving square roots for Chebyshev polynomials
-* Compute zeroes and extrema of Chebyshev polynomials.
-* Prove that the roots of the Chebyshev polynomials (except 0) are irrational.
 -/
 
 @[expose] public section