Theorem Polynomial.Chebyshev.T_derivative_mem_span_T

Modification history

2026-03-10 22:34
Mathlib/RingTheory/Polynomial/Chebyshev.lean
feat(Chebyshev/RootsExtrema): bound iterated derivatives of Chebyshev T on [-1, 1] (#34364)
Added Polynomial.Chebyshev.T_derivative_mem_span_TView on Github →