Skip to content

[Merged by Bors] - feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop#18954

Closed
Command-Master wants to merge 5 commits intomasterfrom
CM_loacwt
Closed

[Merged by Bors] - feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop#18954
Command-Master wants to merge 5 commits intomasterfrom
CM_loacwt

Conversation

@Command-Master
Copy link
Copy Markdown
Collaborator

@Command-Master Command-Master commented Nov 13, 2024

Open in Gitpod

@Command-Master Command-Master added the t-algebra Algebra (groups, rings, fields, etc) label Nov 13, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 13, 2024 •
edited
Loading

PR summary 2bd73c2b52

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ injective_add_left_of_ne_top
+ injective_add_right_of_ne_top
+ strictMono_add_left_of_ne_top
+ strictMono_add_right_of_ne_top
+ sub_pos

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

@Command-Master Command-Master mentioned this pull request Nov 29, 2024
Open
4 tasks
jcommelin
jcommelin reviewed Dec 20, 2024
View reviewed changes
jcommelin
jcommelin reviewed Jan 2, 2025
View reviewed changes
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 2, 2025

✌️ Command-Master 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 the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 2, 2025
@Command-Master
Copy link
Copy Markdown
Collaborator Author

Command-Master commented Jan 4, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jan 4, 2025
@Command-Master
feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCom…
e71f6e9 
…mGroupWithTop (#18954)




Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 4, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop [Merged by Bors] - feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop Jan 4, 2025
@mathlib-bors mathlib-bors bot closed this Jan 4, 2025
@mathlib-bors mathlib-bors bot deleted the CM_loacwt branch January 4, 2025 07:07
Julian added a commit that referenced this pull request Jan 5, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
9857da3 
* origin/master: (133 commits)
  chore(1000): remove nonexistent fields (#20493)
  chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490)
  feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458)
  feat: a conditional kernel is almost everywhere a probability measure (#20430)
  feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304)
  feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479)
  chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492)
  feat(FaaDiBruno): derive `DecidableEq` (#20482)
  chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413)
  chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351)
  chore(MvPolynomial/Localization): golf using TensorProduct (#20309)
  chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277)
  chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259)
  feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091)
  fix: Stop cancelling builds of master (#20435)
  chore: update Mathlib dependencies 2025-01-05 (#20485)
  feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933)
  chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464)
  chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478)
  feat: shorthand lemmas for the L1 norm (#20383)
  chore: remove unnecessary adaptation notes (#20467)
  chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473)
  chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888)
  feat(Algebra): more on `OrthogonalIdempotents` (#18195)
  feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468)
  feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190)
  feat(Algebra/Lie): add Lie's theorem (#13480)
  chore(RingTheory/Generators): make algebra instance a def (#14265)
  feat(Topology/Group): Lemmas about profinite group (#20282)
  feat: the empty set is a topological basis iff the space is empty (#20441)
  chore: make uniqueness of conditionally complete linearly ordered archimedean fields independent of the construction of `Real` (#20242)
  chore: `inherit_doc`s for notations (#20376)
  chore: split AEEqOfIntegral into two files, one for each integral type (#20405)
  chore: split Kernel/MeasurableIntegral (#20427)
  feat(MeasureTheory/Group/Measure): add ContinuousMulEquiv.isHaarMeasure_map (#20469)
  fix(Mathlib.Tactic.CC.Datatypes): `cc` raises panic (#20422)
  feat(Probability/Moments): add lemmas about moment generating functions (#19886)
  feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop (#18954)
  chore: bump toolchain to v4.15.0 (#20461)
  chore: update Mathlib dependencies 2025-01-04 (#20463)
  fix: make `Prod` projection delaborators respond to options, add option to disable (#20455)
  chore(Algebra): Improve attribute generation (#20451)
  feat(Polynomial): `(C a * p).degree = p.degree` if `a * p.leadingCoeff ≠ 0` (#20446)
  feat: add `ENNReal.finStronglyMeasurable_of_measurable` (#20404)
  doc(Algebra/Lie/Weights/Basic): fix typo (#20450)
  chore(1000): remove `identifiers` (#20445)
  feat: add sumPiEquivProdPi and piUnique (#20195)
  feat: add fst_compProd_apply (#20429)
  chore: use unsigned measures for Lebesgue decomposition (#20400)
  feat: Two lemmas on divisibility and coprimality of `expand` (#20143)
  ...
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 left review comments

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

@Command-Master @jcommelin @YaelDillies