[Merged by Bors] - feat: some lemmas on permutation by AntoineChambert-Loir · Pull Request #9359 · leanprover-community/mathlib4

AntoineChambert-Loir · 2023-12-30T18:47:20Z

This PR prepares the way to PR #17046 and #17047 which compute the centralizer of a permutation
in a permutation group and in the alternating group.

depends on: [Merged by Bors] - feat(GroupTheory/Perm/DomMulAct) : Subgroup of Equiv.Perm α preserving a function p : α → ι #9342
depends on: Feat(Algebra/Order/BigOperators/Ring/Multiset): delete duplicate lemmas #16775
depends on: [Merged by Bors] - feat(Algebra/Group/Pi/Lemmas): add Pi.mulSingle_pow #16774
depends on: [Merged by Bors] - feat: lemmas on permutations, cycles, etc. #9602

Mathlib.lean

Mathlib/GroupTheory/Perm/Centralizer.lean

Mathlib.lean

Mathlib/GroupTheory/Perm/Centralizer.lean

jcommelin · 2024-01-09T10:36:52Z

I pushed a bunch of golfing and cleanup of the first ~600 lines to jmc-ConjClassCount. I hope the diff is useful to you.

I think those first ~600 lines of this PR could make a good standalone PR.

riccardobrasca

I know I always say the same thing, but it seems to me there is an easy way of splitting the PR:

you modify three files
new file 1
new file 2

What do you think?

Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean

AntoineChambert-Loir · 2024-09-23T10:24:37Z

@riccardobrasca : I just did what you suggested, there are now two subsequent PR, #17046 and #17047 .

riccardobrasca

Thanks!

bors d+

Mathlib/GroupTheory/Perm/Cycle/Type.lean

Mathlib/GroupTheory/Perm/Cycle/Factors.lean

mathlib-bors · 2024-09-23T10:37:03Z

✌️ AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Mathlib/GroupTheory/Perm/Cycle/Factors.lean

Mathlib/GroupTheory/Perm/DomMulAct.lean

riccardobrasca · 2024-09-26T16:31:37Z

@AntoineChambert-Loir this is almost ready to go. Can you please take into account the last comments? Thanks!

Co-authored-by: Eric Wieser <efw@google.com>

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

Co-authored-by: Eric Wieser <efw@google.com>

AntoineChambert-Loir · 2024-09-27T13:31:49Z

bors r+

This PR prepares the way to PR #17046 and #17047 which compute the centralizer of a permutation in a permutation group and in the alternating group.

mathlib-bors · 2024-09-27T13:57:05Z

Build failed:

Build

AntoineChambert-Loir · 2024-09-27T14:36:57Z

bors r+

This PR prepares the way to PR #17046 and #17047 which compute the centralizer of a permutation in a permutation group and in the alternating group.

mathlib-bors · 2024-09-27T14:46:36Z

Pull request successfully merged into master.

Build succeeded:

This PR prepares the way to PR #17046 and #17047 which compute the centralizer of a permutation in a permutation group and in the alternating group.

Antoine Chambert-Loir added 4 commits December 30, 2023 00:08

initial commit

972be5e

delegate cardinality to ArrowAction

320c553

A working file. Names need to be cleaned up.

e66eedf

adjust Mathlib.lean and import DomMulAct

2b363b8

github-actions bot reviewed Dec 30, 2023

View reviewed changes

Mathlib.lean Show resolved Hide resolved

github-actions bot reviewed Dec 30, 2023

View reviewed changes

AntoineChambert-Loir added WIP Work in progress t-algebra Algebra (groups, rings, fields, etc) labels Dec 30, 2023

avoid the use of finite sets

d9fc7f5

github-actions bot reviewed Dec 30, 2023

View reviewed changes

Mathlib.lean Show resolved Hide resolved

Antoine Chambert-Loir added 4 commits December 31, 2023 00:04

update (linter)

6c2e67d

linter (isolated by)

a42782f

delete ArrowAction

99a506c

update (bad ConjAct.toConjAct)

a59e9af

AntoineChambert-Loir added awaiting-review and removed WIP Work in progress labels Dec 31, 2023

adjust docstring

7c34d07

AntoineChambert-Loir mentioned this pull request Jan 1, 2024

[Merged by Bors] - feat(GroupTheory/Perm/DomMulAct) : Subgroup of Equiv.Perm α preserving a function p : α → ι #9342

Closed

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 6, 2024

Antoine Chambert-Loir added 2 commits January 8, 2024 22:51

merge and adjust DomMulAct

02777f8

adjust sections and docstring

ee2a9c4

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 8, 2024

remove buggy examples, lint100, use factorial notation

9674747

jcommelin reviewed Jan 9, 2024

View reviewed changes

Mathlib/GroupTheory/Perm/Centralizer.lean Outdated Show resolved Hide resolved

jcommelin reviewed Jan 9, 2024

View reviewed changes

Mathlib/GroupTheory/Perm/Centralizer.lean Outdated Show resolved Hide resolved

jcommelin reviewed Jan 9, 2024

View reviewed changes

Mathlib/GroupTheory/Perm/Centralizer.lean Outdated Show resolved Hide resolved

Antoine Chambert-Loir added 2 commits January 9, 2024 11:20

adjust docstring

23f08e6

delete #align lines

13a230c

riccardobrasca reviewed Sep 23, 2024

View reviewed changes

Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean Outdated Show resolved Hide resolved

AntoineChambert-Loir added 2 commits September 23, 2024 12:11

delete the two files that compute the centralizer

0aa44d5

update Mathlib.lean

6d0ee39

This was referenced Sep 23, 2024

[Merged by Bors] - feat: several results on permutations, cycles, etc #17046

Closed

[Merged by Bors] - feat(GroupTheory/SpecificGroups/Alternating/Centralizer): compute the centralizer of a permutation in the alternating group #17047

Closed

AntoineChambert-Loir changed the title ~~feat (GroupTheory/Perm/Centralizer)~~ feat: some lemmas on permutation Sep 23, 2024

riccardobrasca approved these changes Sep 23, 2024

View reviewed changes

Mathlib/GroupTheory/Perm/Cycle/Type.lean Outdated Show resolved Hide resolved

Mathlib/GroupTheory/Perm/Cycle/Factors.lean Outdated Show resolved Hide resolved

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Sep 23, 2024

eric-wieser reviewed Sep 23, 2024

View reviewed changes

Mathlib/GroupTheory/Perm/Cycle/Factors.lean Outdated Show resolved Hide resolved

Mathlib/GroupTheory/Perm/DomMulAct.lean Outdated Show resolved Hide resolved

Mathlib/GroupTheory/Perm/DomMulAct.lean Show resolved Hide resolved

AntoineChambert-Loir and others added 6 commits September 27, 2024 12:28

Update Mathlib/GroupTheory/Perm/DomMulAct.lean

db17d9a

Co-authored-by: Eric Wieser <efw@google.com>

Update Mathlib/GroupTheory/Perm/Cycle/Type.lean

9f30dc2

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

Update Mathlib/GroupTheory/Perm/Cycle/Factors.lean

3273aec

Co-authored-by: Eric Wieser <efw@google.com>

Update Mathlib/GroupTheory/Perm/DomMulAct.lean

3644ea1

Co-authored-by: Eric Wieser <efw@google.com>

make argument implicit; delete double blank lines

d8222dd

restore Fintype

7610e56

mathlib-bors bot pushed a commit that referenced this pull request Sep 27, 2024

feat: some lemmas on permutation (#9359)

e2197ad

This PR prepares the way to PR #17046 and #17047 which compute the centralizer of a permutation in a permutation group and in the alternating group.

Merge branch 'master' into ACL/ConjClassCount

ebcfef3

mathlib-bors bot pushed a commit that referenced this pull request Sep 27, 2024

feat: some lemmas on permutation (#9359)

7abd698

This PR prepares the way to PR #17046 and #17047 which compute the centralizer of a permutation in a permutation group and in the alternating group.

mathlib-bors bot changed the title ~~feat: some lemmas on permutation~~ [Merged by Bors] - feat: some lemmas on permutation Sep 27, 2024

mathlib-bors bot closed this Sep 27, 2024

mathlib-bors bot deleted the ACL/ConjClassCount branch September 27, 2024 14:46

fbarroero pushed a commit that referenced this pull request Oct 2, 2024

feat: some lemmas on permutation (#9359)

d8b8a8f

This PR prepares the way to PR #17046 and #17047 which compute the centralizer of a permutation in a permutation group and in the alternating group.

AntoineChambert-Loir mentioned this pull request Oct 7, 2024

[Merged by Bors] - feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation #17522

Closed

2 tasks

Conversation

AntoineChambert-Loir commented Dec 30, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jcommelin commented Jan 9, 2024

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

AntoineChambert-Loir commented Sep 23, 2024

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Sep 23, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

riccardobrasca commented Sep 26, 2024

Uh oh!

AntoineChambert-Loir commented Sep 27, 2024

Uh oh!

mathlib-bors bot commented Sep 27, 2024

Uh oh!

AntoineChambert-Loir commented Sep 27, 2024

Uh oh!

mathlib-bors bot commented Sep 27, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

AntoineChambert-Loir commented Dec 30, 2023 •

edited

Loading