chore(Algebra/Order/Monoid/Prod): unify type names (#8273)

Co-authored-by: madvorak <dvorakmartinbridge@seznam.cz>
leanprover-community · Nov 8, 2023 · 2f574a6 · 2f574a6
1 parent 83bf88a
commit 2f574a6
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/Mathlib/Algebra/Order/Monoid/Prod.lean b/Mathlib/Algebra/Order/Monoid/Prod.lean
@@ -14,16 +14,16 @@ import Mathlib.Data.Prod.Lex
 
 namespace Prod
 
-variable {α β M N : Type*}
+variable {α β : Type*}
 
 @[to_additive]
 instance [OrderedCommMonoid α] [OrderedCommMonoid β] : OrderedCommMonoid (α × β) where
   mul_le_mul_left _ _ h _ := ⟨mul_le_mul_left' h.1 _, mul_le_mul_left' h.2 _⟩
 
 @[to_additive]
-instance instOrderedCancelCommMonoid [OrderedCancelCommMonoid M] [OrderedCancelCommMonoid N] :
-    OrderedCancelCommMonoid (M × N) :=
-  { (inferInstance : OrderedCommMonoid (M × N)) with
+instance instOrderedCancelCommMonoid [OrderedCancelCommMonoid α] [OrderedCancelCommMonoid β] :
+    OrderedCancelCommMonoid (α × β) :=
+  { (inferInstance : OrderedCommMonoid (α × β)) with
     le_of_mul_le_mul_left :=
       fun _ _ _ h ↦ ⟨le_of_mul_le_mul_left' h.1, le_of_mul_le_mul_left' h.2⟩ }