Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(GroupTheory/GroupAction/Blocks): more on blocks #21284

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat(GroupTheory/GroupAction/Blocks): more on blocks #21284

wants to merge 12 commits into from

Conversation

AntoineChambert-Loir
Copy link
Collaborator

@AntoineChambert-Loir AntoineChambert-Loir commented Jan 31, 2025 •
edited
Loading

  • Some basic results on invariant blocks.
  • The set of blocks containing a given element is a bounded order

Open in Gitpod

@github-actions GitHub Actions
Copy link

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

PR summary 494d190efe

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ BlockMem
+ IsTrivialBlock.image
+ IsTrivialBlock.preimage
+ IsTrivialBlock.smul
+ IsTrivialBlock.smul_iff
+ coe_bot
+ coe_top
+ instance (a : X) : BoundedOrder (BlockMem G a)
+ instance [Nontrivial X] (a : X) : Nontrivial (BlockMem G a) := by

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).

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 31, 2025
@AntoineChambert-Loir AntoineChambert-Loir mentioned this pull request Jan 31, 2025
Closed
8 tasks
YaelDillies
YaelDillies reviewed Jan 31, 2025
View reviewed changes
Mathlib/GroupTheory/GroupAction/Blocks.lean Show resolved Hide resolved
Mathlib/GroupTheory/GroupAction/Blocks.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/GroupAction/Blocks.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/GroupAction/Blocks.lean Outdated Show resolved Hide resolved
@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
Collaborator

@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!

maintainer delegate

Mathlib/GroupTheory/GroupAction/Blocks.lean Outdated Show resolved Hide resolved
@github-actions GitHub Actions
Copy link

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

jcommelin
jcommelin reviewed Jan 31, 2025
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

bors d+

@mathlib-bors
Copy link
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 @YaelDillies
Update Mathlib/GroupTheory/GroupAction/Blocks.lean
494d190 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@AntoineChambert-Loir
Copy link
Collaborator Author

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jan 31, 2025
@AntoineChambert-Loir
feat(GroupTheory/GroupAction/Blocks): more on blocks (#21284)
bf60e81 
- Some basic results on invariant blocks.
- The set of blocks containing a given element is a bounded order
@mathlib-bors
Copy link
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/Blocks): more on blocks [Merged by Bors] - feat(GroupTheory/GroupAction/Blocks): more on blocks Jan 31, 2025
@mathlib-bors mathlib-bors bot closed this Jan 31, 2025
@mathlib-bors mathlib-bors bot deleted the ACL/MoreOnBlocks branch January 31, 2025 20:04
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/Blocks): more on blocks (#21284)
d30d5ec 
- Some basic results on invariant blocks.
- The set of blocks containing a given element is a bounded order
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees
No one assigned
Labels
delegated t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@AntoineChambert-Loir @jcommelin @YaelDillies @leanprover-community-mathlib4-bot