Skip to content

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

Closed
AntoineChambert-Loir wants to merge 12 commits intomasterfrom
ACL/MoreOnBlocks
Closed

[Merged by Bors] - feat(GroupTheory/GroupAction/Blocks): more on blocks#21284
AntoineChambert-Loir wants to merge 12 commits intomasterfrom
ACL/MoreOnBlocks

Conversation

@AntoineChambert-Loir
Copy link
Copy Markdown
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

AntoineChambert-Loir
AntoineChambert-Loir commented Jan 31, 2025
View reviewed changes
@github-actions
Copy link
Copy Markdown

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

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
jcommelin
jcommelin reviewed Jan 31, 2025
View reviewed changes
Copy link
Copy Markdown
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
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 @YaelDillies
Update Mathlib/GroupTheory/GroupAction/Blocks.lean
494d190 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@AntoineChambert-Loir
Copy link
Copy Markdown
Collaborator Author

AntoineChambert-Loir commented Jan 31, 2025

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
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/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 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 @jcommelin @YaelDillies