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

Author: wwylele

Mathlib.lean

@@ -819,6 +819,7 @@ import Mathlib.Algebra.Order.Group.Cyclic
 import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Group.DenselyOrdered
 import Mathlib.Algebra.Order.Group.End
+import Mathlib.Algebra.Order.Group.Equiv
 import Mathlib.Algebra.Order.Group.Finset
 import Mathlib.Algebra.Order.Group.Indicator
 import Mathlib.Algebra.Order.Group.InjSurj
@@ -874,6 +875,7 @@ import Mathlib.Algebra.Order.Kleene
 import Mathlib.Algebra.Order.Module.Algebra
 import Mathlib.Algebra.Order.Module.Basic
 import Mathlib.Algebra.Order.Module.Defs
+import Mathlib.Algebra.Order.Module.Equiv
 import Mathlib.Algebra.Order.Module.Field
 import Mathlib.Algebra.Order.Module.OrderedSMul
 import Mathlib.Algebra.Order.Module.Pointwise

Mathlib/Algebra/Order/Group/Equiv.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2025 Weiyi Wang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Weiyi Wang
+-/
+import Mathlib.Algebra.Group.Equiv.Defs
+import Mathlib.Algebra.Order.Group.Synonym
+
+/-!
+# Add/Mul equivalence for order type synonyms
+-/
+
+variable (α : Type*)
+
+/-- `toLex` as a `MulEquiv`. -/
+@[to_additive "`toLex` as a `AddEquiv`."]
+def toLexMulEquiv [Mul α] : α ≃* Lex α where
+  __ := toLex
+  map_mul' _ _ := by simp
+
+@[to_additive (attr := simp)]
+theorem coe_toLexMulEquiv [Mul α] : ⇑(toLexMulEquiv α) = toLex := rfl
+
+@[to_additive (attr := simp)]
+theorem coe_symm_toLexMulEquiv [Mul α] : ⇑(toLexMulEquiv α).symm = ofLex := rfl
+
+/-- `ofLex` as a `MulEquiv`. -/
+@[to_additive "`ofLex` as a `AddEquiv`."]
+def ofLexMulEquiv [Mul α] : Lex α ≃* α where
+  __ := ofLex
+  map_mul' _ _ := by simp
+
+@[to_additive (attr := simp)]
+theorem coe_ofLexMulEquiv [Mul α] : ⇑(ofLexMulEquiv α) = ofLex := rfl
+
+@[to_additive (attr := simp)]
+theorem coe_symm_ofLexMulEquiv [Mul α] : ⇑(ofLexMulEquiv α).symm = toLex := rfl

Mathlib/Algebra/Order/GroupWithZero/Lex.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 -/
 import Mathlib.Algebra.GroupWithZero.ProdHom
+import Mathlib.Algebra.Order.Group.Equiv
 import Mathlib.Algebra.Order.Hom.MonoidWithZero
 import Mathlib.Algebra.Order.Monoid.Lex
 import Mathlib.Data.Prod.Lex
@@ -25,33 +26,14 @@ Create the "LinOrdCommGrpWithZero" category.
 
 -/
 
--- TODO: find a better place
-/-- `toLex` as a monoid isomorphism. -/
-def toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] : G × H ≃* G ×ₗ H where
-  toFun := toLex
-  invFun := ofLex
-  left_inv := ofLex_toLex
-  right_inv := toLex_ofLex
-  map_mul' := toLex_mul
-
-@[simp]
-lemma coe_toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] :
-    ⇑(toLexMulEquiv G H) = toLex :=
-  rfl
-
-@[simp]
-lemma coe_symm_toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] :
-    ⇑(toLexMulEquiv G H).symm = ofLex :=
-  rfl
-
 @[simp]
 lemma toEquiv_toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] :
-    ⇑(toLexMulEquiv G H : G × H ≃ G ×ₗ H) = toLex :=
+    ⇑(toLexMulEquiv (G × H) : G × H ≃ G ×ₗ H) = toLex :=
   rfl
 
 @[simp]
 lemma toEquiv_symm_toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] :
-    ⇑((toLexMulEquiv G H).symm : G ×ₗ H ≃ G × H) = ofLex :=
+    ⇑((toLexMulEquiv (G × H)).symm : G ×ₗ H ≃ G × H) = ofLex :=
   rfl
 
 namespace MonoidWithZeroHom

Mathlib/Algebra/Order/Module/Equiv.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2025 Weiyi Wang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Weiyi Wang
+-/
+import Mathlib.Algebra.Module.Equiv.Basic
+import Mathlib.Algebra.Order.Group.Equiv
+import Mathlib.Algebra.Order.Module.Synonym
+
+/-!
+# Linear equivalence for order type synonyms
+-/
+
+variable (α β : Type*)
+variable [Semiring α] [AddCommMonoid β] [Module α β]
+
+/-- `toLex` as a linear equivalence -/
+def toLexLinearEquiv : β ≃ₗ[α] Lex β := (toLexAddEquiv β).toLinearEquiv toLex_smul
+
+@[simp]
+theorem coe_toLexLinearEquiv : ⇑(toLexLinearEquiv α β) = toLex := rfl
+
+@[simp]
+theorem coe_symm_toLexLinearEquiv : ⇑(toLexLinearEquiv α β).symm = ofLex := rfl
+
+/-- `ofLex` as a linear equivalence -/
+def ofLexLinearEquiv : Lex β ≃ₗ[α] β := (ofLexAddEquiv β).toLinearEquiv ofLex_smul
+
+@[simp]
+theorem coe_ofLexLinearEquiv : ⇑(ofLexLinearEquiv α β) = ofLex := rfl
+
+@[simp]
+theorem coe_symm_ofLexLinearEquiv : ⇑(ofLexLinearEquiv α β).symm = toLex := rfl