Commit 2020-10-19 10:38 c38d128c

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.