[Merged by Bors] - feat: several results on permutations, cycles, etc#17046
[Merged by Bors] - feat: several results on permutations, cycles, etc#17046AntoineChambert-Loir wants to merge 149 commits intomasterfrom
Conversation
|
I have removed the main new part to another PR (#17522). The present PR consists of basic useful lemmas. |
|
I don't understand what the |
This comment by the bot (which gets updated on each commit) tells you precisely which imports changed (and indeed you add an import in GroupTheory.Perm.Support). In this case I think the import is completely sensible, so no worries (unlike the red color might suggest, this tag is meant to attract attention, not block a PR). |
| (MulAction.stabilizer (ConjAct G) g) := by | ||
| ext k | ||
| simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq, ConjAct.toConjAct_smul] | ||
| rw [eq_comm] |
There was a problem hiding this comment.
Can you check (quickly) if the need for rw [eq_comm] is caused by a lemma written in a way different wrt to the others?
There was a problem hiding this comment.
By mem_centralizer_iff, k belongs to the centralizer of {g} means g * k = k * g, while k belongs to the stabilizer of g by the conjugation action means that k * g * k^{-1} = g.
It probably makes sense to rephrase mem_centralizer_iff in the opposite direction. (But please let
me do that elsewhere!)
There was a problem hiding this comment.
I let a note that maybe we should do that sometime.
|
✌️ AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
|
Pull request successfully merged into master. Build succeeded: |
These are basic results on permutations which will be useful for PR #17522 and #17047 which
study the centralizer of a permutation.