Commit 2021-04-30 20:11 aebe7552
View on Github →refactor(algebra/group_power): put lemmas about order and power in their own file (#7398)
This means group_power/basic has fewer dependencies, making it accessible earlier in the import graph.
The first two lemmas in this basic were moved to the end of order, but otherwise lemmas have been moved without modification and kept in the same order.
The new imports added in other files are the ones needed to make this build.