[Merged by Bors] - chore: Merge `Algebra.Group.Centralizer` into `Algebra.Group.Center` #13034

YaelDillies · 2024-05-19T09:41:58Z

depends on: [Merged by Bors] - chore: Move Invertible #13030
depends on: [Merged by Bors] - feat: generalize Set.inv_mem_center #13921
depends on: [Merged by Bors] - chore: move some lemmas to Algebra.GroupWithZero.Center #13944
depends on: [Merged by Bors] - feat: additivize some Set.center results #14331

github-actions · 2024-05-24T20:27:35Z

- div_mem_center₀
- inv_mem_center₀

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

Ruben-VandeVelde · 2024-06-06T13:24:21Z

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/center.20and.20centralizer

YaelDillies · 2024-06-07T18:13:24Z

Conclusion seems to be that it's fine to merge the files.

github-actions · 2024-06-07T18:14:32Z

PR summary 47b3c1e856

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Group.Centralizer	230	0	-230 (-100.00%)
Mathlib.Algebra.Ring.Centralizer	235	234	-1 (-0.43%)
Mathlib.Algebra.GroupWithZero.Center	236	235	-1 (-0.42%)
Mathlib.GroupTheory.Subsemigroup.Centralizer	369	368	-1 (-0.27%)
Mathlib.Algebra.Star.Center	537	536	-1 (-0.19%)
Mathlib.RingTheory.NonUnitalSubsemiring.Basic	549	548	-1 (-0.18%)
Mathlib.Algebra.Ring.Subsemiring.Basic	568	567	-1 (-0.18%)
Mathlib.Algebra.Ring.CentroidHom	578	577	-1 (-0.17%)

Import changes for all files

Files	Import difference
Too many changes (2095)!

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

From #13034. Co-authored-by: Yaël Dillies <[email protected]>

Ruben-VandeVelde · 2024-06-18T09:11:13Z

I think this is doing too much all at once, so I'll split off some changes the coming days

From #13034. Co-authored-by: Yaël Dillies <[email protected]>

leanprover-community-mathlib4-bot · 2024-07-10T00:10:15Z

This PR/issue depends on:

~~[Merged by Bors] - chore: Move Invertible #13030~~
~~[Merged by Bors] - feat: generalize Set.inv_mem_center #13921~~
~~[Merged by Bors] - chore: move some lemmas to Algebra.GroupWithZero.Center #13944~~
~~[Merged by Bors] - feat: additivize some Set.center results #14331~~
By Dependent Issues (🤖). Happy coding!

Ruben-VandeVelde

lgtm, but I touched this a lot, so please take another look. (Commit by commit might be helpful)

maintainer merge

github-actions · 2024-07-10T16:13:44Z

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

mattrobball · 2024-07-10T16:31:59Z

bors merge

…13034) Co-authored-by: Ruben Van de Velde <[email protected]>

mathlib-bors · 2024-07-10T18:10:31Z

Pull request successfully merged into master.

Build succeeded:

YaelDillies added awaiting-review awaiting-CI t-algebra Algebra (groups, rings, fields, etc) labels May 19, 2024

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label May 19, 2024

github-actions bot removed the awaiting-CI label May 19, 2024

leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label May 23, 2024

YaelDillies force-pushed the split_group_center branch from f269751 to 1a6928d Compare May 23, 2024 08:11

Ruben-VandeVelde added the move-decls label May 24, 2024

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 4, 2024

YaelDillies force-pushed the split_group_center branch from 0f27710 to dc3866d Compare June 4, 2024 17:13

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 4, 2024

Ruben-VandeVelde added awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there and removed awaiting-review labels Jun 6, 2024

YaelDillies added awaiting-review and removed awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there labels Jun 7, 2024

YaelDillies force-pushed the split_group_center branch from dc3866d to d98c56a Compare June 7, 2024 18:13

YaelDillies removed the move-decls label Jun 9, 2024

Ruben-VandeVelde added a commit that referenced this pull request Jun 17, 2024

feat: generalize Set.inv_mem_center

d742bc1

From #13034. Co-authored-by: Yaël Dillies <[email protected]>

Ruben-VandeVelde self-assigned this Jun 17, 2024

Ruben-VandeVelde mentioned this pull request Jun 18, 2024

[Merged by Bors] - feat: generalize Set.inv_mem_center #13921

Closed

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jun 18, 2024

mathlib-bors bot pushed a commit that referenced this pull request Jun 18, 2024

feat: generalize Set.inv_mem_center (#13921)

b04ee70

From #13034. Co-authored-by: Yaël Dillies <[email protected]>

mathlib-bors bot pushed a commit that referenced this pull request Jun 18, 2024

feat: generalize Set.inv_mem_center (#13921)

6f05744

From #13034. Co-authored-by: Yaël Dillies <[email protected]>

leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Jun 18, 2024

kbuzzard pushed a commit that referenced this pull request Jun 26, 2024

feat: generalize Set.inv_mem_center (#13921)

109aaf4

From #13034. Co-authored-by: Yaël Dillies <[email protected]>

mathlib-bors bot pushed a commit that referenced this pull request Jul 1, 2024

chore: move some lemmas to Algebra.GroupWithZero.Center (#13944)

336da1d

From #13034. Co-authored-by: Yaël Dillies <[email protected]>

mathlib-bors bot pushed a commit that referenced this pull request Jul 1, 2024

chore: move some lemmas to Algebra.GroupWithZero.Center (#13944)

0b99fcc

From #13034. Co-authored-by: Yaël Dillies <[email protected]>

leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Jul 1, 2024

YaelDillies force-pushed the split_group_center branch from 8df53b3 to d4121c8 Compare July 1, 2024 12:24

leanprover-community-mathlib4-bot added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jul 1, 2024

dagurtomas pushed a commit that referenced this pull request Jul 2, 2024

chore: move some lemmas to Algebra.GroupWithZero.Center (#13944)

ac61d4a

From #13034. Co-authored-by: Yaël Dillies <[email protected]>

kim-em removed the awaiting-review label Jul 9, 2024

leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jul 10, 2024

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 10, 2024

Ruben-VandeVelde added 3 commits July 10, 2024 06:11

chore: target explicitness adjustments

d79a9d5

chore: use sections consistently

4260619

chore: Split Algebra.Group.Center

47b3c1e

YaelDillies force-pushed the split_group_center branch from d4121c8 to 47b3c1e Compare July 10, 2024 06:11

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 10, 2024

Ruben-VandeVelde changed the title ~~chore: Split Algebra.Group.Center~~ chore: Merge Algebra.Group.Centralizer into Algebra.Group.Center Jul 10, 2024

Ruben-VandeVelde approved these changes Jul 10, 2024

View reviewed changes

github-actions bot added the maintainer-merge label Jul 10, 2024

github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 10, 2024

mathlib-bors bot pushed a commit that referenced this pull request Jul 10, 2024

chore: Merge Algebra.Group.Centralizer into Algebra.Group.Center (#…

c6cc81d

…13034) Co-authored-by: Ruben Van de Velde <[email protected]>

mathlib-bors bot changed the title ~~chore: Merge Algebra.Group.Centralizer into Algebra.Group.Center~~ [Merged by Bors] - chore: Merge Algebra.Group.Centralizer into Algebra.Group.Center Jul 10, 2024

mathlib-bors bot closed this Jul 10, 2024

mathlib-bors bot deleted the split_group_center branch July 10, 2024 18:10

adomani mentioned this pull request Aug 1, 2024

feat: MiM PR report #15355

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: Merge `Algebra.Group.Centralizer` into `Algebra.Group.Center` #13034

[Merged by Bors] - chore: Merge `Algebra.Group.Centralizer` into `Algebra.Group.Center` #13034

YaelDillies commented May 19, 2024 •

edited by Ruben-VandeVelde

Loading

github-actions bot commented May 24, 2024

Ruben-VandeVelde commented Jun 6, 2024

YaelDillies commented Jun 7, 2024

github-actions bot commented Jun 7, 2024 •

edited

Loading

Import changes for modified files

Ruben-VandeVelde commented Jun 18, 2024

leanprover-community-mathlib4-bot commented Jul 10, 2024

Ruben-VandeVelde left a comment

github-actions bot commented Jul 10, 2024

mattrobball commented Jul 10, 2024

mathlib-bors bot commented Jul 10, 2024

[Merged by Bors] - chore: Merge Algebra.Group.Centralizer into Algebra.Group.Center #13034

[Merged by Bors] - chore: Merge Algebra.Group.Centralizer into Algebra.Group.Center #13034

Conversation

YaelDillies commented May 19, 2024 • edited by Ruben-VandeVelde Loading

github-actions bot commented May 24, 2024

Ruben-VandeVelde commented Jun 6, 2024

YaelDillies commented Jun 7, 2024

github-actions bot commented Jun 7, 2024 • edited Loading

PR summary 47b3c1e856

Import changes for modified files

Declarations diff

Ruben-VandeVelde commented Jun 18, 2024

leanprover-community-mathlib4-bot commented Jul 10, 2024

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

github-actions bot commented Jul 10, 2024

mattrobball commented Jul 10, 2024

mathlib-bors bot commented Jul 10, 2024

[Merged by Bors] - chore: Merge `Algebra.Group.Centralizer` into `Algebra.Group.Center` #13034

[Merged by Bors] - chore: Merge `Algebra.Group.Centralizer` into `Algebra.Group.Center` #13034

YaelDillies commented May 19, 2024 •

edited by Ruben-VandeVelde

Loading

github-actions bot commented Jun 7, 2024 •

edited

Loading