[Merged by Bors] - chore: use mixin ordered algebraic typeclasses (part 2)#20595
Closed
astrainfinita wants to merge 197 commits intomasterfrom
Closed
[Merged by Bors] - chore: use mixin ordered algebraic typeclasses (part 2)#20595astrainfinita wants to merge 197 commits intomasterfrom
astrainfinita wants to merge 197 commits intomasterfrom
Conversation
commit 7561e65e55f1dbba1058c43ca1701038ceed98dc Author: negiizhao <[email protected]> Date: Wed Jun 5 04:26:04 2024 +0800 fix commit 777db8a7d19ed4d66815f9575206992ca578cb5e Merge: cc6eede 52b851a Author: negiizhao <[email protected]> Date: Wed Jun 5 04:25:36 2024 +0800 Merge branch 'master' into FR_canonically commit cc6eede Author: negiizhao <[email protected]> Date: Thu Dec 28 15:01:00 2023 +0800 fix commit ae1dfda Merge: c1931cf 1a749e0 Author: negiizhao <[email protected]> Date: Thu Dec 28 14:10:05 2023 +0800 Merge branch 'FR_covariance_instance' into FR_canonically commit c1931cf Merge: 9e0f667 6cab3d6 Author: negiizhao <[email protected]> Date: Thu Dec 28 14:09:53 2023 +0800 Merge branch 'master' into FR_canonically commit 1a749e0 Author: negiizhao <[email protected]> Date: Tue Dec 26 04:24:52 2023 +0800 revert some instance changes commit a6e645f Author: negiizhao <[email protected]> Date: Mon Dec 25 11:01:06 2023 +0800 fix commit 6af13a5 Author: negiizhao <[email protected]> Date: Mon Dec 25 10:06:19 2023 +0800 Revert "fix" This reverts commit 7ebd135. commit 63a181b Author: negiizhao <[email protected]> Date: Mon Dec 25 09:49:50 2023 +0800 hack commit 7ebd135 Author: negiizhao <[email protected]> Date: Sun Dec 24 14:25:47 2023 +0800 fix commit 20d2809 Author: negiizhao <[email protected]> Date: Sun Dec 24 14:13:08 2023 +0800 chore: remove redundant instances commit 9e0f667 Author: negiizhao <[email protected]> Date: Sun Dec 24 12:45:15 2023 +0800 fix commit bf51f25 Merge: bd9e5b4 e9fb5b3 Author: negiizhao <[email protected]> Date: Sun Dec 24 12:00:56 2023 +0800 Merge branch 'master' into FR_canonically commit bd9e5b4 Author: negiizhao <[email protected]> Date: Tue Oct 24 01:49:05 2023 +0800 nolint again commit 6414331 Author: negiizhao <[email protected]> Date: Tue Oct 24 00:36:00 2023 +0800 reduce diffs commit 6d1f059 Author: negiizhao <[email protected]> Date: Mon Oct 23 19:41:50 2023 +0800 Revert "remove nolint" This reverts commit d60fc68. commit d60fc68 Author: negiizhao <[email protected]> Date: Mon Oct 23 10:24:07 2023 +0800 remove nolint commit 86f6ec7 Author: negiizhao <[email protected]> Date: Mon Oct 23 10:23:24 2023 +0800 fix commit a3d8af1 Merge: 58e2ba8 801dc0d Author: negiizhao <[email protected]> Date: Mon Oct 23 09:53:43 2023 +0800 Merge branch 'master' into FR_canonically commit 58e2ba8 Author: negiizhao <[email protected]> Date: Mon Oct 23 09:52:49 2023 +0800 reduce diffs commit be2b4bb Author: negiizhao <[email protected]> Date: Mon Oct 23 08:58:03 2023 +0800 `[Mul α] [LE α]` -> `[Monoid α] [PartialOrder α]` commit 0777b07 Author: negiizhao <[email protected]> Date: Mon Oct 23 02:46:01 2023 +0800 rerun bench please commit 6415bc9 Author: negiizhao <[email protected]> Date: Sun Oct 22 18:30:20 2023 +0800 fix commit 14cdac7 Author: negiizhao <[email protected]> Date: Sun Oct 22 14:11:31 2023 +0800 nolint commit 5bc0815 Author: Mario Carneiro <[email protected]> Date: Sat Oct 21 17:30:57 2023 -0400 chore: bump lean toolchain commit 86c8440 Author: negiizhao <[email protected]> Date: Sat Oct 21 23:50:53 2023 +0800 fix commit f14bdc9 Author: negiizhao <[email protected]> Date: Sat Oct 21 23:07:59 2023 +0800 fix commit 5feb528 Author: negiizhao <[email protected]> Date: Sat Oct 21 22:41:09 2023 +0800 fix commit 958c4a5 Author: negiizhao <[email protected]> Date: Sat Oct 21 22:07:26 2023 +0800 fix commit fae1c85 Author: negiizhao <[email protected]> Date: Fri Oct 20 21:07:44 2023 +0800 fix commit e6309d6 Author: negiizhao <[email protected]> Date: Fri Oct 20 20:07:09 2023 +0800 fix merge commit a619670 Author: negiizhao <[email protected]> Date: Fri Oct 20 20:06:29 2023 +0800 oops commit 9c3d72d Author: negiizhao <[email protected]> Date: Fri Oct 20 20:04:15 2023 +0800 fix merge commit 8a76d2e Author: negiizhao <[email protected]> Date: Fri Oct 20 20:01:16 2023 +0800 fix merge commit 7793f03 Author: negiizhao <[email protected]> Date: Fri Oct 20 19:59:08 2023 +0800 fix commit 659f503 Author: negiizhao <[email protected]> Date: Fri Oct 20 18:59:49 2023 +0800 fix merge commit a259cc5 Author: negiizhao <[email protected]> Date: Fri Oct 20 18:54:10 2023 +0800 fix commit d6eb31f Author: negiizhao <[email protected]> Date: Fri Oct 20 18:18:02 2023 +0800 fix commit 2650679 Author: negiizhao <[email protected]> Date: Fri Oct 20 16:31:11 2023 +0800 fix commit 5bfb9ec Merge: c5279c0 08a8af0 Author: negiizhao <[email protected]> Date: Fri Oct 20 16:19:14 2023 +0800 Merge branch 'master' into FR_canonically commit c5279c0 Author: negiizhao <[email protected]> Date: Mon Aug 7 02:47:06 2023 +0800 lint commit 19a377f Author: negiizhao <[email protected]> Date: Thu Aug 3 16:57:10 2023 +0800 lint commit 048b120 Author: negiizhao <[email protected]> Date: Thu Aug 3 15:43:32 2023 +0800 fix counterexamples commit 94663ee Author: negiizhao <[email protected]> Date: Thu Aug 3 14:22:22 2023 +0800 lint style commit 426dd03 Author: negiizhao <[email protected]> Date: Thu Aug 3 14:00:46 2023 +0800 refactor: make `CanonicallyOrdered...` mixin I think this is the proposed refactor. However it seems that all things get slower... :( Need more love to speed it up.
Collaborator
|
Here are the benchmark results for commit ec6b1cc. Benchmark Metric Change
=============================================================================
- ~Mathlib.Algebra.Order.CauSeq.Basic instructions 16.6%
- ~Mathlib.Algebra.Order.Floor instructions 50.8%
- ~Mathlib.Algebra.Order.ToIntervalMod instructions 54.2%
- ~Mathlib.Analysis.Convex.Deriv instructions 20.8%
- ~Mathlib.Analysis.Convex.Jensen instructions 20.4%
- ~Mathlib.Analysis.Convex.Mul instructions 21.0%
- ~Mathlib.Analysis.Convex.Side instructions 12.5%
+ ~Mathlib.Analysis.MeanInequalitiesPow instructions -20.5%
- ~Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform instructions 25.1%
+ ~Mathlib.LinearAlgebra.Orientation instructions -15.5%
+ ~Mathlib.Topology.Algebra.Field instructions -29.7%
- ~Mathlib.Topology.Instances.AddCircle instructions 20.0% |
3 files, Instructions +11.0⬝10⁹
2 files, Instructions +8.0⬝10⁹
3 files, Instructions +7.0⬝10⁹
3 files, Instructions +5.0⬝10⁹
4 files, Instructions +4.0⬝10⁹
7 files, Instructions +3.0⬝10⁹
10 files, Instructions +2.0⬝10⁹
24 files, Instructions +1.0⬝10⁹
61 files, Instructions -2.0⬝10⁹
18 files, Instructions -3.0⬝10⁹
11 files, Instructions -4.0⬝10⁹
4 files, Instructions -5.0⬝10⁹
6 files, Instructions -6.0⬝10⁹
3 files, Instructions -8.0⬝10⁹
2 files, Instructions -10.0⬝10⁹
|
leanprover-community-bot-assistant
added
the
merge-conflict
Contributor
|
Coming here from PR triage: I'm aware this PR is mainly waiting for maintainer review - but for the record, let me also point out that there is a merge conflict. Thanks for this PR; I hope your entire series can land in mathlib soon. |
github-actions
bot
removed
the
merge-conflict
kbuzzard
reviewed
Apr 6, 2025
kbuzzard
approved these changes
Apr 7, 2025
Collaborator
|
This pull request has conflicts, please merge |
leanprover-community-bot-assistant
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
Member
|
Thanks! bors merge |
ghost
added
the
Contributor
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
tannerduve
pushed a commit
that referenced
this pull request
May 13, 2025
1 task
mathlib-bors bot
pushed a commit
that referenced
this pull request
Oct 14, 2025
… a single ring of scalars (#29342) Currently the definition of Absolutely Convex in Mathlib is a little unexpected: ``` def AbsConvex (s : Set E) : Prop := Balanced 𝕜 s ∧ Convex ℝ s ``` At the time this definition was formulated, Mathlib's definition of `Convex` required the scalars to be an `OrderedSemiring` whereas the definition of `Balanced` required the scalars to be a `SeminormedRing`. Mathlib didn't have a concept of a semi-normed ordered ring, so a set was defined as `AbsConvex` if it is balanced over a `SeminormedRing` `𝕜` and convex over `ℝ`. Recently the requirements for the definition of `Convex` have been relaxed (#24392, #20595) so it is now possible to use a single scalar ring in common with the literature. Previous discussion: - #17029 (comment) - #26345 (comment)
Jlh18
pushed a commit
to Jlh18/mathlib4
that referenced
this pull request
Oct 24, 2025
… a single ring of scalars (leanprover-community#29342) Currently the definition of Absolutely Convex in Mathlib is a little unexpected: ``` def AbsConvex (s : Set E) : Prop := Balanced 𝕜 s ∧ Convex ℝ s ``` At the time this definition was formulated, Mathlib's definition of `Convex` required the scalars to be an `OrderedSemiring` whereas the definition of `Balanced` required the scalars to be a `SeminormedRing`. Mathlib didn't have a concept of a semi-normed ordered ring, so a set was defined as `AbsConvex` if it is balanced over a `SeminormedRing` `𝕜` and convex over `ℝ`. Recently the requirements for the definition of `Convex` have been relaxed (leanprover-community#24392, leanprover-community#20595) so it is now possible to use a single scalar ring in common with the literature. Previous discussion: - leanprover-community#17029 (comment) - leanprover-community#26345 (comment)
BeibeiX0
pushed a commit
to BeibeiX0/mathlib4
that referenced
this pull request
Nov 7, 2025
… a single ring of scalars (leanprover-community#29342) Currently the definition of Absolutely Convex in Mathlib is a little unexpected: ``` def AbsConvex (s : Set E) : Prop := Balanced 𝕜 s ∧ Convex ℝ s ``` At the time this definition was formulated, Mathlib's definition of `Convex` required the scalars to be an `OrderedSemiring` whereas the definition of `Balanced` required the scalars to be a `SeminormedRing`. Mathlib didn't have a concept of a semi-normed ordered ring, so a set was defined as `AbsConvex` if it is balanced over a `SeminormedRing` `𝕜` and convex over `ℝ`. Recently the requirements for the definition of `Convex` have been relaxed (leanprover-community#24392, leanprover-community#20595) so it is now possible to use a single scalar ring in common with the literature. Previous discussion: - leanprover-community#17029 (comment) - leanprover-community#26345 (comment)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
7 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
diff