[Merged by Bors] - feat(GroupTheory/GroupAction): new FixedPoints module with a few basic properties of fixedBy
#9477
Conversation
…group is a subset This is a theorem that is needed for the proof of Rubin's theorem, and it sets the ground up for discussions about implementing a separate `movingSubgroup` definition.
…gation and pointwise SMul Namely: - `fixedBy_mul`, `movedBy_mul` - `fixedBy_conj`, `movedBy_conj` - `smul_pow_mem_of_movedBy_subset` and its corollaries - `smul_pow_mem_movedBy_of_commute` and its corollaries
…o smul_mem_of_movedBy_subset
adri326
added
t-algebra
adri326
added
the
awaiting-review
jcommelin
added
awaiting-author
…s.lean and FixingSubgroup.lean Signed-off-by: Adrien Burgun <adrien.burgun@orange.fr>
|
I fixed the above issues; the CI should pass, as I haven't changed any public-facing interfaces. |
adri326
added
awaiting-review
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
|
I fixed the issues pointed out by @riccardobrasca, as well as some I noticed in the meantime (some theorems were named I would like to say that trying to get this first pull request merged has been a pretty demotivating experience so far: The backlog of pull requests means that each round of small issue that could be caught ahead of time with proper tooling instead adds at least a day before this pull request gets approved. I understand the need to have PRs be properly reviewed, but I long for tools to reduce these reviews down to the more impactful issues. |
I am sorry this has been a painful experience. One thing to keep in mind is that last week there was a pretty important Lean conference, so a lot of people didn't have time to review PRs: we know that it is a slow process, but maybe you were just unlucky. Can you please copy/paste this message on Zulip? It is very possible that some of tools you want exist, but are maybe not very well documented (for example you can run all the linters locally, it is just slow). |
If you have enough local compute Automatic code formatting is definitely on the roadmap! |
…and simplify theorems using pointwise smul
…complement of fixedBy This is in an effort to keep definitions simp-normal: `movedBy α g` meant that simp lemmas need to be duplicated between `fixedBy` and `movedBy`.
|
I replaced This was quite the refactor so I wouldn't be surprised if I accidentally re-introduced small issues in there. |
adri326
changed the title
MulAction.movedBy and a few basic properties of fixedBy and movedByFixedPoints module with a few basic properties of fixedBy
|
@tb65536 haven't heard back in a little while, are there other design patterns that are problematic with this PR? |
|
LGTM! Thanks for adding all this API maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by tb65536. |
|
(I guess it should be delegated, since CI is still running) |
leanprover-community-mathlib4-bot
added
ready-to-merge
…sic properties of `fixedBy` (#9477) Introduces a new module, `Mathlib.GroupTheory.GroupAction.FixedPoints`, which contains some properties of `MulAction.fixedBy` that wouldn't quite belong to `Mathlib.GroupTheory.GroupAction.Basic`.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
FixedPoints module with a few basic properties of fixedByFixedPoints module with a few basic properties of fixedBy
…sic properties of `fixedBy` (#9477) Introduces a new module, `Mathlib.GroupTheory.GroupAction.FixedPoints`, which contains some properties of `MulAction.fixedBy` that wouldn't quite belong to `Mathlib.GroupTheory.GroupAction.Basic`.
Introduces a new module,
Mathlib.GroupTheory.GroupAction.FixedPoints,which contains some properties of
MulAction.fixedBythat wouldn't quite belong toMathlib.GroupTheory.GroupAction.Basic.This is my first contribution ever to Mathlib, and the first contribution in a series of contributions to eventually merge my formalization of Rubin's theorem into Lean.
I have a few questions around the design decisions that I took:
shouldmovedBybe defined inMathlib.GroupTheory.GroupAction.Basicinstead?Mathlib.GroupTheory.GroupAction.FixingSubgroupusesMfor a group, would it be out-of-scope for this PR to also replace it withG?not_commute_of_disjoint_movedBy_preimagemight be too out-of-scope