Merge branch 'FR_setoid_instance' into FR_quotient_mk''_abbrev

leanprover-community · Sep 2, 2024 · 8d146de · 8d146de
2 parents 94d8cdc + a92336b
commit 8d146de
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Data/Quot.lean b/Mathlib/Data/Quot.lean
@@ -328,7 +328,7 @@ theorem surjective_quotient_mk {α : Sort*} (s : Setoid α) :
   Quot.exists_rep
 
 /-- `Quotient.mk'` is a surjective function. -/
-theorem surjective_quotient_mk' (α : Sort*) {s : Setoid α} :
+theorem surjective_quotient_mk' (α : Sort*) [s : Setoid α] :
     Function.Surjective (Quotient.mk' : α → Quotient s) :=
   Quot.exists_rep