fix(Algebra/Bounds): generalize index type to sort (#12113)

leanprover-community · Apr 13, 2024 · a0cb217 · a0cb217
1 parent 7a71e52
commit a0cb217
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Algebra/Bounds.lean b/Mathlib/Algebra/Bounds.lean
@@ -189,7 +189,7 @@ end Right
 
 section Left
 
-variable {ι G : Type*} [Group G] [ConditionallyCompleteLattice G]
+variable {ι : Sort*} {G : Type*} [Group G] [ConditionallyCompleteLattice G]
   [CovariantClass G G (· * ·) (· ≤ ·)] [Nonempty ι] {f : ι → G}
 
 @[to_additive]