From 1f111f99c93930b12e157887045ba978c588f8e3 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Fri, 16 Jan 2026 12:36:11 +0200 Subject: [PATCH 1/2] Update documentation --- .../Trigonometric/Chebyshev/RootsExtrema.lean | 4 ++++ Mathlib/RingTheory/Polynomial/Chebyshev.lean | 2 -- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean index 63d836fc1a79ed..7d0afd453f70d7 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean +++ b/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. -/ @[expose] public section diff --git a/Mathlib/RingTheory/Polynomial/Chebyshev.lean b/Mathlib/RingTheory/Polynomial/Chebyshev.lean index a27d83b7b9a8d1..c3804fbf514a08 100644 --- a/Mathlib/RingTheory/Polynomial/Chebyshev.lean +++ b/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. * Prove minimax properties of Chebyshev polynomials. -/ From 6f0daea7ea1b5eda87d70194407a4dc69fbae729 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Fri, 16 Jan 2026 23:01:22 +0200 Subject: [PATCH 2/2] Update TODO --- Mathlib/RingTheory/Polynomial/Chebyshev.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/RingTheory/Polynomial/Chebyshev.lean b/Mathlib/RingTheory/Polynomial/Chebyshev.lean index 4375a4bee6c4e9..5a164fe2757426 100644 --- a/Mathlib/RingTheory/Polynomial/Chebyshev.lean +++ b/Mathlib/RingTheory/Polynomial/Chebyshev.lean @@ -54,7 +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 -* Prove minimax properties of Chebyshev polynomials. -/ @[expose] public section