mathlib3
1dd69d30 - refactor(data/polynomial): re-organizing (#3512)

Commit
6 years ago
refactor(data/polynomial): re-organizing (#3512) This builds on #3407, trying to get related material closer together. There shouldn't be any change to the set of declarations, just the order they come in and the imports required to get them. The major changes are: 1. `data.polynomial.derivative` now has much weaker imports 2. generally, material has been moved "upwards" to the first place it can be done (a lot of material moved out of `data.polynomial.degree` into `data.polynomial.degree.basic` -- essentially `degree` is the material about `degree` that also needs `eval` and friends; a further rename might be appropriate) 3. some of the later material is no longer a big chain of linear dependencies, but compiles separately Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Author
Parents
Loading