mathlib

aebe7552 - refactor(algebra/group_power): put lemmas about order and power in their own file (#7398)

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.