chore(Algebra/Order): generalise ordered algebra lemmas (#37040)

artie2000 · artie2000 · commit 4609a29824f4 · 2026-04-01T19:38:34.000Z
* Generalise lemmas from ordered algebras to ordered modules + mixins
diff --git a/Mathlib/Algebra/Order/Algebra.lean b/Mathlib/Algebra/Order/Algebra.lean
@@ -39,47 +39,48 @@ public section
 
 variable {α β : Type*} [CommSemiring α] [PartialOrder α] [Semiring β] [PartialOrder β] [Algebra α β]
 
-section OrderedSemiring
-variable (β) [IsOrderedRing β] [SMulPosMono α β] {a : α}
+section ZeroLEOneClass
+variable [ZeroLEOneClass β]
 
-@[gcongr, mono] lemma algebraMap_mono : Monotone (algebraMap α β) :=
-  fun a₁ a₂ ha ↦ by
-    simpa only [Algebra.algebraMap_eq_smul_one] using smul_le_smul_of_nonneg_right ha zero_le_one
+section SMulPosMono
+variable (β) [SMulPosMono α β]
 
-lemma algebraMap_nonneg (ha : 0 ≤ a) : 0 ≤ algebraMap α β a := by simpa using algebraMap_mono β ha
+@[gcongr, mono]
+lemma algebraMap_mono : Monotone (algebraMap α β) := by
+  simpa [Algebra.smul_def] using smul_one_mono (α := α) β
 
-end OrderedSemiring
+lemma algebraMap_nonneg {a : α} (ha : 0 ≤ a) : 0 ≤ algebraMap α β a := by
+  simpa using algebraMap_mono β ha
 
-section StrictOrderedSemiring
-variable [IsStrictOrderedRing β]
+end SMulPosMono
 
-section SMulPosMono
-variable [SMulPosMono α β] [SMulPosReflectLE α β] {a₁ a₂ : α}
+section Nontrivial
+variable [Nontrivial β]
 
-@[simp] lemma algebraMap_le_algebraMap : algebraMap α β a₁ ≤ algebraMap α β a₂ ↔ a₁ ≤ a₂ := by
+@[simp]
+lemma algebraMap_le_algebraMap [SMulPosMono α β] [SMulPosReflectLE α β] {a₁ a₂ : α} :
+    algebraMap α β a₁ ≤ algebraMap α β a₂ ↔ a₁ ≤ a₂ := by
   simp [Algebra.algebraMap_eq_smul_one]
 
-end SMulPosMono
-
 section SMulPosStrictMono
-variable [SMulPosStrictMono α β] {a a₁ a₂ : α}
-variable (β)
+variable (β) [SMulPosStrictMono α β]
 
-@[gcongr, mono] lemma algebraMap_strictMono : StrictMono (algebraMap α β) :=
-  fun a₁ a₂ ha ↦ by
-    simpa only [Algebra.algebraMap_eq_smul_one] using smul_lt_smul_of_pos_right ha zero_lt_one
+@[gcongr, mono]
+lemma algebraMap_strictMono : StrictMono (algebraMap α β) := by
+  simpa [Algebra.smul_def] using smul_one_strictMono (α := α) β
 
-lemma algebraMap_pos (ha : 0 < a) : 0 < algebraMap α β a := by
+lemma algebraMap_pos {a : α} (ha : 0 < a) : 0 < algebraMap α β a := by
   simpa using algebraMap_strictMono β ha
 
-variable {β}
-variable [SMulPosReflectLT α β]
-
-@[simp] lemma algebraMap_lt_algebraMap : algebraMap α β a₁ < algebraMap α β a₂ ↔ a₁ < a₂ := by
+variable {β} in
+@[simp]
+lemma algebraMap_lt_algebraMap [SMulPosReflectLT α β] {a₁ a₂ : α} :
+    algebraMap α β a₁ < algebraMap α β a₂ ↔ a₁ < a₂ := by
   simp [Algebra.algebraMap_eq_smul_one]
 
 end SMulPosStrictMono
-end StrictOrderedSemiring
+end Nontrivial
+end ZeroLEOneClass
 
 namespace Mathlib.Meta.Positivity
 open Lean Meta Qq Function
diff --git a/Mathlib/Algebra/Order/Module/Defs.lean b/Mathlib/Algebra/Order/Module/Defs.lean
@@ -360,6 +360,12 @@ lemma strictMono_smul_right_of_pos [SMulPosStrictMono α β] (hb : 0 < b) :
 @[gcongr] lemma smul_le_smul_of_nonneg_right [SMulPosMono α β] (ha : a₁ ≤ a₂) (hb : 0 ≤ b) :
     a₁ • b ≤ a₂ • b := monotone_smul_right_of_nonneg hb ha
 
+variable (β) in
+@[gcongr, mono]
+lemma smul_one_mono [One β] [ZeroLEOneClass β] [SMulPosMono α β] :
+    Monotone (fun x : α ↦ x • (1 : β)) :=
+  fun _ _ ha ↦ smul_le_smul_of_nonneg_right ha zero_le_one
+
 @[gcongr] lemma smul_lt_smul_of_pos_right [SMulPosStrictMono α β] (ha : a₁ < a₂) (hb : 0 < b) :
     a₁ • b < a₂ • b := strictMono_smul_right_of_pos hb ha
 
@@ -422,6 +428,13 @@ lemma smul_le_smul' [PosSMulMono α β] [SMulPosMono α β] (ha : a₁ ≤ a₂)
 end LeftRight
 end Preorder
 
+variable (β) in
+@[gcongr, mono]
+lemma smul_one_strictMono [Preorder α] [PartialOrder β] [Zero β] [One β] [ZeroLEOneClass β]
+    [NeZero (1 : β)] [SMulPosStrictMono α β] :
+    StrictMono (fun x : α ↦ x • (1 : β)) :=
+  fun _ _ ha ↦ smul_lt_smul_of_pos_right ha (zero_lt_one (α := β))
+
 section PartialOrder
 variable [Semiring α] [PartialOrder α]
 
