-
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] - refactor(algebra/group_power): put lemmas about order and power in their own file #7398
Conversation
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
…eir own file 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 copied and kept in the same order.
…roup_power # Conflicts: # src/algebra/group_power/basic.lean
39c0e6d
to
bfea112
Compare
bors r+ |
…eir 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.
Build failed (retrying...): |
I think this conflicts with #7140, let's see whether that one goes in before cancelling this one |
I took that one off the queue since it didn't build with |
…eir 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.
Pull request successfully merged into master. Build succeeded: |
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 oforder
, 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.
sq
as convention for "squared" #7368This will conflict with #7368