feat: port RingTheory.Perfection (#4629)

Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
leanprover-community · Jun 11, 2023 · b29c8d1 · b29c8d1
1 parent a01c6e8
commit b29c8d1
Show file tree

Hide file tree

Showing 3 changed files with 659 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2444,6 +2444,7 @@ import Mathlib.RingTheory.NonUnitalSubsemiring.Basic
 import Mathlib.RingTheory.NonZeroDivisors
 import Mathlib.RingTheory.OreLocalization.Basic
 import Mathlib.RingTheory.OreLocalization.OreSet
+import Mathlib.RingTheory.Perfection
 import Mathlib.RingTheory.Polynomial.Basic
 import Mathlib.RingTheory.Polynomial.Bernstein
 import Mathlib.RingTheory.Polynomial.Chebyshev

diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean
@@ -302,7 +302,7 @@ instance [Nontrivial R] : Nontrivial (FractionRing R) :=
 
 /-- Porting note: if the fields of this instance are explicitly defined as they were
 in mathlib3, the last instance in this file suffers a TC timeout -/
-noncomputable instance : Field (FractionRing A) := IsFractionRing.toField A
+noncomputable instance field : Field (FractionRing A) := IsFractionRing.toField A
 
 @[simp]
 theorem mk_eq_div {r s} :