mathlib3
3309ce27 - refactor(ring_theory/polynomial/chebyshev): move lemmas around (#6510)

Commit
4 years ago
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`.
Author
Parents
Loading