[Merged by Bors] - feat(Algebra/Order): LinearEquiv version of toLex/ofLex

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,43 @@
+/-
+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*) [Mul α]
+
+/-- `toLex` as a `MulEquiv`. -/
+@[to_additive "`toLex` as a `AddEquiv`."]
+def toLexMulEquiv : α ≃* Lex α where
+  toEquiv := toLex
+  map_mul' _ _ := by simp
+
+/-- `ofLex` as a `MulEquiv`. -/
+@[to_additive "`ofLex` as a `AddEquiv`."]
+def ofLexMulEquiv : Lex α ≃* α where
+  toEquiv := ofLex
+  map_mul' _ _ := by simp
+
+@[to_additive (attr := simp)]
+theorem coe_toLexMulEquiv : ⇑(toLexMulEquiv α) = toLex := rfl
+
+@[to_additive (attr := simp)]
+theorem coe_ofLexMulEquiv : ⇑(ofLexMulEquiv α) = ofLex := rfl
+
+@[to_additive (attr := simp)]
+lemma symm_toLexMulEquiv : (toLexMulEquiv α).symm = ofLexMulEquiv α := rfl
+
+@[to_additive (attr := simp)]
+lemma symm_ofLexMulEquiv : (ofLexMulEquiv α).symm = toLexMulEquiv α := rfl
+
+@[to_additive (attr := simp)]
+lemma toEquiv_toLexMulEquiv : (toLexMulEquiv α : α ≃ Lex α) = toLex := rfl
+
+@[to_additive (attr := simp)]
+lemma toEquiv_ofLexMulEquiv : (ofLexMulEquiv α : Lex α ≃ α) = ofLex := rfl

Mathlib/Algebra/Order/GroupWithZero/Lex.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 -/
 import Mathlib.Algebra.GroupWithZero.ProdHom
-import Mathlib.Algebra.Order.Hom.MonoidWithZero
+import Mathlib.Algebra.Order.Group.Equiv
 import Mathlib.Algebra.Order.Monoid.Lex
+import Mathlib.Algebra.Order.Hom.MonoidWithZero
 import Mathlib.Data.Prod.Lex
 
 /-!
@@ -25,35 +26,6 @@ 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 :=
-  rfl
-
-@[simp]
-lemma toEquiv_symm_toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] :
-    ⇑((toLexMulEquiv G H).symm : G ×ₗ H ≃ G × H) = ofLex :=
-  rfl
-
 namespace MonoidWithZeroHom
 
 variable {M₀ N₀ : Type*}

Mathlib/Algebra/Order/Module/Equiv.lean

@@ -0,0 +1,27 @@
+/-
+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
+
+/-- `ofLex` as a linear equivalence -/
+def ofLexLinearEquiv : Lex β ≃ₗ[α] β := (ofLexAddEquiv β).toLinearEquiv ofLex_smul
+
+@[simp] lemma coe_toLexLinearEquiv : ⇑(toLexLinearEquiv α β) = toLex := rfl
+@[simp] lemma coe_ofLexLinearEquiv : ⇑(ofLexLinearEquiv α β) = ofLex := rfl
+
+@[simp] lemma symm_toLexLinearEquiv : (toLexLinearEquiv α β).symm = ofLexLinearEquiv α β := rfl
+@[simp] lemma symm_ofLexLinearEquiv : (ofLexLinearEquiv α β).symm = toLexLinearEquiv α β := rfl