Theorem Polynomial.Chebyshev.two_mul_T_eq_U_sub_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.two_mul_T_eq_U_sub_UView on Github →