-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(algebra/char_zero): split #17760
Conversation
bors d+ |
✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with |
@semorrison I fixed a timing-out calc block in the tests by breaking the calc into two. I hope this still tests what it's supposed to (it's in |
bors merge |
Split `algebra/char_zero` into `algebra/char_zero/lemmas` and `algebra/char_zero/infinite` (there was already a `algebra/char_zero/defs`), with the former not importing finset. As intended, this caused a few files which had been getting their finset import by this path to require that import explicitly. I've added the finset imports explicitly on all such files, except for `tactic/positivity`, the point being that I actually want to remove the finset import from positivity. I moved the `fin{set,type}.card` positivity extensions from `tactic/positivity` to `data/fintype/card`.
Pull request successfully merged into master. Build succeeded: |
Split
algebra/char_zero
intoalgebra/char_zero/lemmas
andalgebra/char_zero/infinite
(there was already aalgebra/char_zero/defs
), with the former not importing finset.As intended, this caused a few files which had been getting their finset import by this path to require that import explicitly. I've added the finset imports explicitly on all such files, except for
tactic/positivity
, the point being that I actually want to remove the finset import from positivity. I moved thefin{set,type}.card
positivity extensions fromtactic/positivity
todata/fintype/card
.