Theorem Polynomial.Chebyshev.integral_measureT_eq_integral_cos_of_continuous

Modification history

2026-03-23 08:24
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean
feat: more versions of the change of variables formula for monotone functions (#36855) …
Deleted Polynomial.Chebyshev.integral_measureT_eq_integral_cos_of_continuousView on Github →
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_measureT_eq_integral_cos_of_continuousView on Github →