From 0d7dd61a2e5e58e4d8fd0f721c5ac039f7075da4 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Wed, 13 May 2026 10:43:44 +0100 Subject: [PATCH] perf: Field.toEuclideanDomain fast_instance% --- Mathlib/Algebra/EuclideanDomain/Field.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/EuclideanDomain/Field.lean b/Mathlib/Algebra/EuclideanDomain/Field.lean index 3ba135fab0f1ae..b9ca7ccf17e034 100644 --- a/Mathlib/Algebra/EuclideanDomain/Field.lean +++ b/Mathlib/Algebra/EuclideanDomain/Field.lean @@ -9,6 +9,8 @@ public import Mathlib.Algebra.EuclideanDomain.Defs public import Mathlib.Algebra.Field.Defs public import Mathlib.Algebra.GroupWithZero.Units.Basic +import Mathlib.Tactic.FastInstance + /-! # Instances for Euclidean domains * `Field.toEuclideanDomain`: shows that any field is a Euclidean domain. @@ -21,7 +23,7 @@ namespace Field variable {K : Type*} [Field K] -- see Note [lower instance priority] -instance (priority := 100) toEuclideanDomain : EuclideanDomain K := +instance (priority := 100) toEuclideanDomain : EuclideanDomain K := fast_instance% { toCommRing := toCommRing quotient := (· / ·), remainder := fun a b => a - a * b / b, quotient_zero := div_zero, quotient_mul_add_remainder_eq := fun a b => by