change order of commRing and divisionRing in field

leanprover-community · Dec 22, 2024 · 53313de · 53313de
1 parent 49dbf9e
commit 53313de
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/RingTheory/Ideal/Quotient/Basic.lean b/Mathlib/RingTheory/Ideal/Quotient/Basic.lean
@@ -138,8 +138,8 @@ will have computable inverses (and `qsmul`, `ratCast`) in some applications.
 See note [reducible non-instances]. -/
 protected noncomputable abbrev field {R} [CommRing R] (I : Ideal R) [I.IsMaximal] :
     Field (R ⧸ I) where
-  __ := Quotient.divisionRing I
   __ := commRing _
+  __ := Quotient.divisionRing I
 
 /-- If the quotient by an ideal is a field, then the ideal is maximal. -/
 theorem maximal_of_isField {R} [CommRing R] (I : Ideal R) (hqf : IsField (R ⧸ I)) :