-
Notifications
You must be signed in to change notification settings - Fork 262
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: change Subgroup
and Submonoid
induction principles to work with induction
#9861
Conversation
In fact I only need the `closure` lemma, but the others are easy enough.
…with `induction`
Subgroup
and Submonoid
induction principles to work with induction
This PR/issue depends on: |
…-induction-dependent
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a great improvement, thanks!
LGTM, module @_adomani's comment. bors d+ |
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…with `induction` (#9861) Induction principles have to be fully dependent in order to work with the `induction` tactic. This is usually a good thing anyway, since the dependent version is often more convenient to use, and avoids the caller having to fumble with generalizing over an existential. This changes the following induction principles (and their additive versions): * `Submonoid.closure_induction_{left,right}` * `Subgroup.closure_induction_{left,right}` * `Subgroup.closure_induction''` (no submonoid version exists) Arguments to these lemmas have also been renamed to drop the `H`, as seems to be preferred for `induction` lemmas.
Pull request successfully merged into master. Build succeeded: |
Subgroup
and Submonoid
induction principles to work with induction
Subgroup
and Submonoid
induction principles to work with induction
…with `induction` (#9861) Induction principles have to be fully dependent in order to work with the `induction` tactic. This is usually a good thing anyway, since the dependent version is often more convenient to use, and avoids the caller having to fumble with generalizing over an existential. This changes the following induction principles (and their additive versions): * `Submonoid.closure_induction_{left,right}` * `Subgroup.closure_induction_{left,right}` * `Subgroup.closure_induction''` (no submonoid version exists) Arguments to these lemmas have also been renamed to drop the `H`, as seems to be preferred for `induction` lemmas.
…with `induction` (#9861) Induction principles have to be fully dependent in order to work with the `induction` tactic. This is usually a good thing anyway, since the dependent version is often more convenient to use, and avoids the caller having to fumble with generalizing over an existential. This changes the following induction principles (and their additive versions): * `Submonoid.closure_induction_{left,right}` * `Subgroup.closure_induction_{left,right}` * `Subgroup.closure_induction''` (no submonoid version exists) Arguments to these lemmas have also been renamed to drop the `H`, as seems to be preferred for `induction` lemmas.
Induction principles have to be fully dependent in order to work with the
induction
tactic. This is usually a good thing anyway, since the dependent version is often more convenient to use, and avoids the caller having to fumble with generalizing over an existential.This changes the following induction principles (and their additive versions):
Submonoid.closure_induction_{left,right}
Subgroup.closure_induction_{left,right}
Subgroup.closure_induction''
(no submonoid version exists)Arguments to these lemmas have also been renamed to drop the
H
, as seems to be preferred forinduction
lemmas.Sub{group,monoid}.{op,unop}
#9860