Skip to content

[Merged by Bors] - feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions#21285

Closed
AntoineChambert-Loir wants to merge 4 commits intomasterfrom
ACL/MoreOnTransitive
Closed

[Merged by Bors] - feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions#21285
AntoineChambert-Loir wants to merge 4 commits intomasterfrom
ACL/MoreOnTransitive

Conversation

@AntoineChambert-Loir
Copy link
Copy Markdown
Collaborator

@AntoineChambert-Loir AntoineChambert-Loir commented Jan 31, 2025

Open in Gitpod

@AntoineChambert-Loir AntoineChambert-Loir mentioned this pull request Jan 31, 2025
Closed
8 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 31, 2025 •
edited
Loading

PR summary 96c449ace5

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.GroupTheory.GroupAction.Transitive (new file) 434

Declarations diff

+ IsPretransitive.of_surjective_map
+ isPretransitive_congr
+ isPretransitive_iff_base
+ isPretransitive_iff_orbit_eq_top

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@YaelDillies YaelDillies self-assigned this Jan 31, 2025
YaelDillies
YaelDillies reviewed Jan 31, 2025
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2025
@AntoineChambert-Loir AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2025
YaelDillies
YaelDillies approved these changes Jan 31, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for splitting!

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 31, 2025

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 31, 2025
@YaelDillies YaelDillies added the t-algebra Algebra (groups, rings, fields, etc) label Jan 31, 2025
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Jan 31, 2025

Thanks!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 31, 2025

✌️ 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.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jan 31, 2025
@AntoineChambert-Loir
Copy link
Copy Markdown
Collaborator Author

AntoineChambert-Loir commented Jan 31, 2025

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 31, 2025

✌️ 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.

AntoineChambert-Loir
AntoineChambert-Loir commented Jan 31, 2025
View reviewed changes
Copy link
Copy Markdown
Collaborator Author

@AntoineChambert-Loir AntoineChambert-Loir left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

comments on docstrings

@AntoineChambert-Loir
Copy link
Copy Markdown
Collaborator Author

AntoineChambert-Loir commented Jan 31, 2025

bors r+

1 similar comment
@AntoineChambert-Loir
Copy link
Copy Markdown
Collaborator Author

AntoineChambert-Loir commented Jan 31, 2025

bors r+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 31, 2025

Already running a review

mathlib-bors bot pushed a commit that referenced this pull request Jan 31, 2025
@AntoineChambert-Loir
feat(GroupTheory/GroupAction/Transitive): basic results on transitive…
e58d6d7 
… actions (#21285)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 31, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions [Merged by Bors] - feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions Jan 31, 2025
@mathlib-bors mathlib-bors bot closed this Jan 31, 2025
@mathlib-bors mathlib-bors bot deleted the ACL/MoreOnTransitive branch January 31, 2025 13:11
Julian added a commit that referenced this pull request Feb 2, 2025
@Julian
Merge branch 'factorial-dvd-int' into bhargava-factorial
4aa075f 
* factorial-dvd-int: (143 commits)
  Apply suggestions from code review
  feat(Factorial): k! divides the product of any k successive integers
  feat(CategoryTheory): creation of finite limits (#21320)
  chore: update Mathlib dependencies 2025-02-01 (#21328)
  chore(GroupTheory/SpecificGroups/Alternating.lean): follow last minute review of JX (#21314)
  feat: `‖x‖ₑ.toNNReal = ‖x‖₊` (#21306)
  chore: cleanup imports in Archive/IfNormalization (#21318)
  doc: fix several typos (#21315)
  feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310)
  chore: delete declarations deprecated between 2024-01 and 2024-07 (#21271)
  feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule (#20084)
  chore(Data/ZMod/Basic): split `ZMod.valMinAbs` off (#21308)
  feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522)
  feat(RingTheory/LocalRing): `IsLocalRing` for subrings (#21168)
  chore: update Mathlib dependencies 2025-02-01 (#21312)
  chore: update Mathlib dependencies 2025-01-31 (#21311)
  feat: generalize `mem_dite` to `Membership α β` (#21262)
  feat: Lemmas for some monomial orders (#16177)
  feat(CategoryTheory): the localized category is monoidal (#12728)
  feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289)
  feat(RingTheory/WittVector): ring of Witt vectors is p-adically complete (#21295)
  feat(GroupTheory/GroupAction/Blocks): more on blocks (#21284)
  fix(FieldTheory/KrullTopology): make `krullTopology_discreteTopology_of_finiteDimensional` universe polymorphic (#21299)
  feat(RingTheory/Artinian): integral non-zero-divisors are units over artinian rings (#21199)
  refactor(Topology/Gluing): simplify definition of `TopCat.GlueData.Rel` (#20653)
  feat(RingTheory/PowerSeries): binomial series (#20192)
  chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff  (#21290)
  chore (RingTheory/HahnSeries): fix names that use coeff (#21279)
  feat: let `notation3` distinguish `Prop` vs `Type _ ` vs `Sort _` (#21233)
  chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273)
  feat(CategoryTheory): the monoidal category structure on a localization (#20951)
  feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem (#15009)
  feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328)
  feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` (#14486)
  feat: Function.const as a PartialEquiv (#21137)
  chore(NonZeroDivisors): don't import rings (#20871)
  feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267)
  feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190)
  feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions (#21285)
  perf(MeasureTheory/Function/LpSpace.lean): speed up (#21179)
  feat(Order): order isomorphisms from `Fin n` for small `n` (#21120)
  refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740)
  feat: Sylow's first theorem for elementary `p`-groups (#21072)
  chore(Submonoid/Membership): don't import `MonoidWithZero` (#20748)
  refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213)
  feat(GroupTheory/IndexNormal): subgroups of small index are normal (#21186)
  feat(Algebra/Group/Action): add definition of equidecomposition (#16936)
  feat(CategoryTheory/Subpresheaf): equalizer (#21096)
  feat: add lemmas about products of `Matrix.stdBasisMatrix` (#21204)
  chore: update Mathlib dependencies 2025-01-31 (#21282)
  ...
jt496 pushed a commit that referenced this pull request Feb 3, 2025
@AntoineChambert-Loir @jt496
feat(GroupTheory/GroupAction/Transitive): basic results on transitive…
5773660 
… actions (#21285)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

@YaelDillies YaelDillies

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@AntoineChambert-Loir @riccardobrasca @YaelDillies