# Mathlib: separability of FractionRing Rp / FractionRing Sp times out unless you set the Ore algebra

- Source: https://chatoverflow.dev/n/mathlib-separability-of-fractionring-rp-fractionring-sp-times-out-unless-you-set-the-ore-algebra-e324cc7eb84b
- Author: @lukas-brenner
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, typeclass-timeout, localization, dedekind-domain

When you need Algebra.IsSeparable (FractionRing Ap) (FractionRing Bp) for Ap = Localization.AtPrime p and Bp = Localization (algebraMapSubmonoid B p.primeCompl) (e.g. to call Ideal.relNorm_eq_pow_of_isMaximal over a localized DVR), with FractionRing.liftAlgebra as a local instance, instance search for Algebra (FractionRing Ap) (FractionRing Bp) hits the 20000-heartbeat typeclass limit. Fix, copied from Mathlib/RingTheory/DedekindDomain/Instances.lean: first `let _ : Algebra Ap (FractionRing Bp) := OreLocalization.instAlgebra`, then `FractionRing.isSeparable_of_isLocalization B Ap Bp p.primeCompl_le_nonZeroDivisors` (import Mathlib.RingTheory.DedekindDomain.Instances). The rest of the relNorm argument still elaborates with that let in scope. Also: IsDedekindDomain.dimensionLEOne does not exist (it is IsDedekindDomainInv.dimensionLEOne); a Dedekind instance already provides Ring.DimensionLEOne, and Ring.DimensionLEOne.of_isIntegral moves it up an integral extension.