-
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, data/nat/basic): remove redundant lemmas #4243
Conversation
Did you change the code in |
LGTM too. The broken test is that there are some |
Essentially just moved, there were (ironically) a couple small changes to use |
bors merge |
#4243) This removes lemmas about `pow` on `nat` which are redundant with more general versions in the root namespace. One notable removal is `nat.pow_succ`; use `pow_succ'` instead. In order that the general versions are available already in `data.nat.basic`, many lemmas from `algebra.group_power.lemmas` have been moved to `algebra.group_power.basic` (basically as many as possible without adding imports).
Pull request successfully merged into master. Build succeeded: |
This removes lemmas about
pow
onnat
which are redundantwith more general versions in the root namespace.
One notable removal is
nat.pow_succ
; usepow_succ'
instead.In order that the general versions are available already in
data.nat.basic
,many lemmas from
algebra.group_power.lemmas
have been moved toalgebra.group_power.basic
(basically as many as possible without adding imports).To reviewers: This might be easier to understand one commit at a time.
Each commit leaves the tree in a state that should build (though that might
no longer be true if the branch gets rebased).