[Merged by Bors] - feat: lemmas on permutations, cycles, etc.#9602
Closed
AntoineChambert-Loir wants to merge 50 commits intomasterfrom
Closed
[Merged by Bors] - feat: lemmas on permutations, cycles, etc.#9602AntoineChambert-Loir wants to merge 50 commits intomasterfrom
AntoineChambert-Loir wants to merge 50 commits intomasterfrom
Conversation
4 tasks
Member
riccardobrasca
left a comment
There was a problem hiding this comment.
Mathlib/GroupTheory/Perm/Cycle/Basic.lean is getting super long and we should probably split it (in another PR), especially taking into account the new linter.
urkud
reviewed
Jan 23, 2024
Member
|
I've merged master. |
Member
|
The new linter fired up, so I guess you have to split the file in another PR and then we can merge this one. |
Collaborator
Author
|
What do you mean? |
Member
|
That the linter is saying |
Member
|
Note that I just kicked #10035 on the queue (I am not sure if it is relevant here). |
riccardobrasca
approved these changes
Sep 17, 2024
| {a : α} (ha : p a) : (ofSubtype (g.subtypePerm hg)) a = g a := | ||
| ofSubtype_apply_of_mem (g.subtypePerm hg) ha | ||
|
|
||
| theorem ofSubtype_subtypePerm_of_not_mem {p : α → Prop} [DecidablePred p] |
Contributor
|
✌️ AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with |
Collaborator
Author
|
bors r+ |
Member
|
Can you please take into account my last comments? Thanks! (Feel free to merge it once done with those.) bors r- |
Collaborator
Author
|
sorry to have missed your comments. |
Member
No worries! |
Member
|
Thanks! bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Sep 18, 2024
This PR establishes various lemmas in the theory of permutation groups, pertaining to the supports, cycle decompositions, and the conjugation action of `ConjAct (Equiv.Perm α)` on `Equiv.Perm α` This lemmas stem out PR #9359 and are used there to compute the cardinalities of the conjugacy classes of permutations. Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
6 participants
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.
This PR establishes various lemmas in the theory of permutation groups,
pertaining to the supports, cycle decompositions, and the conjugation action
of
ConjAct (Equiv.Perm α)onEquiv.Perm αThis lemmas stem out PR #9359 and are used there to compute the cardinalities
of the conjugacy classes of permutations.