[Merged by Bors] - feat(Algebra/Order): `LinearEquiv` version of `toLex`/`ofLex` by wwylele · Pull Request #27711 · leanprover-community/mathlib4

wwylele · 2025-07-31T01:41:11Z

github-actions · 2025-07-31T01:42:25Z

PR summary cdda99e28c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Order.GroupWithZero.Lex`	1
`Mathlib.Algebra.Order.Group.Equiv` (new file)	181
`Mathlib.Algebra.Order.Module.Equiv` (new file)	509

Declarations diff

+ coe_ofLexLinearEquiv
+ coe_ofLexMulEquiv
+ coe_toLexLinearEquiv
+ ofLexLinearEquiv
+ ofLexMulEquiv
+ symm_ofLexLinearEquiv
+ symm_ofLexMulEquiv
+ symm_toLexLinearEquiv
+ symm_toLexMulEquiv
+ toEquiv_ofLexMulEquiv
+ toLexLinearEquiv
- coe_symm_toLexMulEquiv
- toEquiv_symm_toLexMulEquiv

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

pechersky · 2025-07-31T10:48:41Z

I think the existing lemmas about coercion from MulEquiv to Equiv should also be moved to the new file.

wwylele · 2025-07-31T17:42:30Z

I moved toEquiv_toLexMulEquiv and toEquiv_symm_toLexMulEquiv mostly as-is, though I don't quite understand their purpose. They seems to be just repeat of coe_toLexMulEquiv and coe_symm_toLexMulEquiv with an additional intermediate coe...

Mathlib/Algebra/Order/Group/Equiv.lean

pechersky · 2025-07-31T23:45:59Z

Specifically for the lemmas that coerce to Equiv, you shouldn't have the outer coercion lemma. Because if you do, that statement becomes about coercions to functions.

wwylele · 2025-07-31T23:48:33Z

Oh yeah that's also what confused me, because the original code had ⇑. I'll remove it

pechersky · 2025-07-31T23:51:14Z

Yeah the original code, written by me, was wrong!

Mathlib/Algebra/Order/Group/Equiv.lean

YaelDillies · 2025-08-06T18:08:13Z

Mathlib/Algebra/Order/Group/Equiv.lean

+variable (α : Type*)
+
+/-- `toLex` as a `MulEquiv`. -/
+@[to_additive "`toLex` as a `AddEquiv`."]


Suggested change

@[to_additive "`toLex` as a `AddEquiv`."]

@[to_additive (attr := simps toEquiv) "`toLex` as a `AddEquiv`."]

This produces toLexMulEquiv_toEquiv, which is basically renaming toEquiv_toLexMulEquiv. (toEquiv_toLexMulEquiv was introduced in #22420). This is where I don't know what our naming convention is and I found both examples in the library. toEquiv can be seen as a function application so the function name should appear first; but there are also example where a dot member is written the other way.

For things which ""are clearly projections"", the name tends to come last. At any rate, simps producing that name is good authority to follow

Got it. I have applied the change and removed toEquiv_toLexMulEquiv

Welp, the simp normal form checker rejected this

-- Mathlib.Algebra.Order.Group.Equiv Error: /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/Mathlib/Algebra/Order/Group/Equiv.lean:16:24: error: toLexMulEquiv_toEquiv Left-hand side simplifies from (toLexMulEquiv α).toEquiv to ↑(toLexMulEquiv α) using dsimp only [*, @MulEquiv.toEquiv_eq_coe] Try to change the left-hand side to the simplified term!

Ugh, I'm so sorry my suggestion depends on #21031

Mathlib/Algebra/Order/Group/Equiv.lean

This reverts commit aef0962.

Mathlib/Algebra/Order/Module/Equiv.lean

Mathlib/Algebra/Order/Group/Equiv.lean

YaelDillies

Thanks!

maintainer delegate

Mathlib/Algebra/Order/Group/Equiv.lean

github-actions · 2025-08-08T06:16:26Z

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

bryangingechen · 2025-08-09T19:43:43Z

Thanks!
bors r+

mathlib-bors · 2025-08-09T19:55:31Z

Pull request successfully merged into master.

Build succeeded:

CI Success

…over-community#27711)

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jul 31, 2025

wwylele force-pushed the wwylele-hahn-lex branch from fd6e0f0 to 2c98ade Compare July 31, 2025 02:19

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jul 31, 2025

wwylele force-pushed the wwylele-hahn-lex branch 3 times, most recently from 5d0c49b to 29b924b Compare July 31, 2025 02:56

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Jul 31, 2025

feat(Algebra/Order): Add Add/Mul/Linear equiv versions of toLex/ofLex

494d834

wwylele force-pushed the wwylele-hahn-lex branch from 29b924b to 494d834 Compare July 31, 2025 02:59

wwylele added 2 commits July 31, 2025 13:39

move lemma

92b50a0

move

3f414a0

pechersky reviewed Jul 31, 2025

View reviewed changes

Mathlib/Algebra/Order/Group/Equiv.lean Outdated Show resolved Hide resolved

wwylele added 3 commits July 31, 2025 17:58

simplify

5a400ed

to_additive

3ef1834

shake

4e50811

remove coerce

e13603f

wwylele mentioned this pull request Aug 1, 2025

[Merged by Bors] - feat(Algebra/Order): Hahn embedding theorem, part 1 #27043

Closed

7 tasks

YaelDillies reviewed Aug 6, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 6, 2025

wwylele added 2 commits August 6, 2025 15:46

address comments

3b3f5cb

address comments

aef0962

wwylele removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 6, 2025

Revert "address comments"

d529836

This reverts commit aef0962.

YaelDillies reviewed Aug 7, 2025

View reviewed changes

Mathlib/Algebra/Order/Module/Equiv.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/Order/Group/Equiv.lean Outdated Show resolved Hide resolved

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 7, 2025

adjust symm simp

2116674

wwylele removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 7, 2025

YaelDillies changed the title ~~feat(Algebra/Order): Add Add/Mul/Linear equiv versions of toLex/ofLex~~ feat(Algebra/Order): LinearEquiv version of toLex/ofLex Aug 8, 2025

YaelDillies approved these changes Aug 8, 2025

View reviewed changes

Mathlib/Algebra/Order/Group/Equiv.lean Outdated Show resolved Hide resolved

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 8, 2025

wwylele added 2 commits August 8, 2025 09:38

extract Mul to variable

7843b71

remove extra space

242bb00

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Aug 9, 2025

mathlib-bors bot pushed a commit that referenced this pull request Aug 9, 2025

feat(Algebra/Order): LinearEquiv version of toLex/ofLex (#27711)

8afc93b

mathlib-bors bot changed the title ~~feat(Algebra/Order): LinearEquiv version of toLex/ofLex~~ [Merged by Bors] - feat(Algebra/Order): LinearEquiv version of toLex/ofLex Aug 9, 2025

mathlib-bors bot closed this Aug 9, 2025

thorimur pushed a commit to thorimur/mathlib4 that referenced this pull request Aug 11, 2025

feat(Algebra/Order): LinearEquiv version of toLex/ofLex (leanpr…

dc38382

…over-community#27711)

Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025

feat(Algebra/Order): LinearEquiv version of toLex/ofLex (leanpr…

46a36d9

…over-community#27711)

wwylele deleted the wwylele-hahn-lex branch September 2, 2025 01:32

	@[to_additive "`toLex` as a `AddEquiv`."]
	@[to_additive (attr := simps toEquiv) "`toLex` as a `AddEquiv`."]

Conversation

wwylele commented Jul 31, 2025

Uh oh!

github-actions bot commented Jul 31, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary cdda99e28c

Import changes for modified files

Declarations diff

Uh oh!

pechersky commented Jul 31, 2025

Uh oh!

wwylele commented Jul 31, 2025

Uh oh!

Uh oh!

pechersky commented Jul 31, 2025

Uh oh!

wwylele commented Jul 31, 2025

Uh oh!

pechersky commented Jul 31, 2025

Uh oh!

Uh oh!

YaelDillies Aug 6, 2025

Choose a reason for hiding this comment

Uh oh!

wwylele Aug 6, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Aug 6, 2025

Choose a reason for hiding this comment

Uh oh!

wwylele Aug 6, 2025

Choose a reason for hiding this comment

Uh oh!

wwylele Aug 6, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Aug 7, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Aug 8, 2025

Uh oh!

bryangingechen commented Aug 9, 2025

Uh oh!

mathlib-bors bot commented Aug 9, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions bot commented Jul 31, 2025 •

edited

Loading