Skip to content

Commit 66fd97d

Browse files
kbuzzardb-mehta
authored andcommitted
perf(RingTheory/LaurentSeries): add some instances (leanprover-community#39186)
Typeclass inference was expensively failing at some point in `LaurentSeries.valuation_compare` without these instances.
1 parent 07abf15 commit 66fd97d

1 file changed

Lines changed: 8 additions & 0 deletions

File tree

Mathlib/RingTheory/LaurentSeries.lean

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -992,6 +992,14 @@ abbrev extensionAsRingHom :=
992992
/-- An abbreviation for the `X`-adic completion of `K⟮X⟯` -/
993993
abbrev RatFuncAdicCompl := adicCompletion K⟮X⟯ (idealX K)
994994

995+
-- help typeclass inference along
996+
instance : Field (ratfuncAdicComplPkg (K := K).space) :=
997+
inferInstanceAs <| Field (RatFuncAdicCompl K)
998+
999+
-- help typeclass inference along
1000+
instance : Valued (ratfuncAdicComplPkg (K := K).space) (WithZero (Multiplicative ℤ)) :=
1001+
inferInstanceAs <| Valued (RatFuncAdicCompl K) (WithZero (Multiplicative ℤ))
1002+
9951003
/- The two instances below make `comparePkg` and `comparePkg_eq_extension` slightly faster. -/
9961004
instance : UniformSpace (RatFuncAdicCompl K) := inferInstance
9971005
instance : UniformSpace K⸨X⸩ := inferInstance

0 commit comments

Comments
 (0)