Commit 2021-03-03 10:36 3309ce27
View on Github →refactor(ring_theory/polynomial/chebyshev): move lemmas around (#6510)
As discussed in #6501, split up the old file ring_theory.polynomial.chebyshev.basic, moving half its contents to ring_theory.polynomial.chebyshev.defs and the other half to ring_theory.polynomial.chebyshev.dickson.