mathlib
54c432da - chore(algebra/parity): Reduce imports (#17391)

Commit
3 years ago
chore(algebra/parity): Reduce imports (#17391) This PR takes the stance that `algebra.parity` is a basic pure algebra file, and thus moves all the `zpow` material to `algebra.field.basic` and `algebra.order.field.power`, and the `irreducible` material to `algebra.associated`.
Author
Parents
Loading