Theorem Polynomial.Chebyshev.U_eq_two_mul_T_add_U

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.U_eq_two_mul_T_add_UView on Github →