[Merged by Bors] - refactor(group_theory/group_action): Break the file into three pieces #4936
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
I found myself fighting import cycles when trying to define `has_scalar` instances on primitive types. By creating a separate `defs` file with minimal dependencies, this ought to become easier. This also renames some lemmas, namely: * `mul_action.inv_smul_smul` → `inv_smul_smul` (the one on `group α`) * `inv_smul_smul` → `inv_smul_smul'` (the one on `group_with_zero α`) The documentation is new too. None of the proofs or lemma statements have been touched.
eric-wieser
added
the
awaiting-review
eric-wieser
force-pushed
the
split-group_action
branch
from
1ddc60d
to
208af0f
Compare
This renames * `mul_action.inv_smul_eq_iff` → `inv_smul_eq_iff` (the one on `group α`). This makes it consistent with `smul_neg` etc, which are in the global scope * `inv_smul_eq_iff` → `inv_smul_eq_iff'` (the one on `group_with_zero α`). This makes it consistent with `smul_inv_smul'`, which has a trailing `'`
eric-wieser
added
the
blocked-by-other-PR
Closed
1 task
eric-wieser
commented
Nov 9, 2020
Comment on lines
+8
to
+12
| import group_theory.coset | ||
|
|
||
| /-! | ||
| # Basic properties of group actions | ||
| -/ |
There was a problem hiding this comment.
The main reason this file is separate from group_theory.group_action.group is that the coset import pulls in quite a deep tree.
There was a problem hiding this comment.
Do you mind expanding the module doc with the main definitions and theorems?
There was a problem hiding this comment.
I don't really have the background to pick out the "main" ones - so I'd be inclined to just put this in, and let someone with more background fill out the docs
There was a problem hiding this comment.
OK, no worries.
bors r+
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
eric-wieser
removed
the
blocked-by-other-PR
bryangingechen
approved these changes
Nov 11, 2020
Comment on lines
+8
to
+12
| import group_theory.coset | ||
|
|
||
| /-! | ||
| # Basic properties of group actions | ||
| -/ |
There was a problem hiding this comment.
Do you mind expanding the module doc with the main definitions and theorems?
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
bryangingechen
added
delegated
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
bors bot
pushed a commit
that referenced
this pull request
Nov 11, 2020
…#4936) I found myself fighting import cycles when trying to define `has_scalar` instances in files that are early in the import tree. By creating a separate `defs` file with minimal dependencies, this ought to become easier. This also adds documentation. None of the proofs or lemma statements have been touched.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I found myself fighting import cycles when trying to define
has_scalarinstances in files that are early in the import tree.By creating a separate
defsfile with minimal dependencies, this ought to become easier.This also adds documentation.
None of the proofs or lemma statements have been touched.
I imagine this will take a few tries to pass CI. It's quite easy to accidentally change the typeclasses in the enclosing
section/namespacefor a lemma, which breaks applications elsewhere.