mathlib3

c38d128c - feat(ring_theory/polynomial/chebyshev): chebyshev polynomials of the first kind (#4267)

feat(ring_theory/polynomial/chebyshev): chebyshev polynomials of the first kind (#4267) If T_n denotes the n-th Chebyshev polynomial of the first kind, then the polynomials 2*T_n(X/2) form a Lambda structure on Z[X]. I call these polynomials the lambdashev polynomials, because, as far as I am aware they don't have a name in the literature. We show that they commute, and that the p-th polynomial is congruent to X^p mod p. In other words: a Lambda structure. Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com> Co-authored-by: Reid Barton <rwbarton@gmail.com> Co-authored-by: none <none> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>