Theorem Polynomial.Chebyshev.integral_T_real_mul_self_measureT_of_ne_zero

Modification history

2026-01-27 17:10
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean
feat(Chebyshev/Orthogonality): Chebyshev T polynomials are orthogonal (#33676) …
Added Polynomial.Chebyshev.integral_T_real_mul_self_measureT_of_ne_zeroView on Github →