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] - feat(group_theory/subgroup/basic): a new to_additive lemma, and remove a by hand proof #9594
Conversation
…e a lemma generated by to_additive
Thanks! bors merge |
…e a by hand proof (#9594) I needed `add_subgroup.smul_mem` which didn't seem to exist, and noticed that the `add_subgroup.gsmul_mem` version is proved by hand while to_additive generates it fine (now?)
bors r+ |
…e a by hand proof (#9594) I needed `add_subgroup.smul_mem` which didn't seem to exist, and noticed that the `add_subgroup.gsmul_mem` version is proved by hand while to_additive generates it fine (now?)
Build failed (retrying...): |
…e a by hand proof (#9594) I needed `add_subgroup.smul_mem` which didn't seem to exist, and noticed that the `add_subgroup.gsmul_mem` version is proved by hand while to_additive generates it fine (now?)
bors r- |
Canceled. |
bors d+ Thanks! |
✌️ alexjbest can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…e a by hand proof (#9594) I needed `add_subgroup.smul_mem` which didn't seem to exist, and noticed that the `add_subgroup.gsmul_mem` version is proved by hand while to_additive generates it fine (now?)
Pull request successfully merged into master. Build succeeded: |
I needed
add_subgroup.smul_mem
which didn't seem to exist, and noticed that theadd_subgroup.gsmul_mem
version is proved by hand while to_additive generates it fine (now?)