English
Let R be a commutative ring and K be a commutative ring with an R-algebra structure. Then K is the localization of R at the multiplicative set of non-zero divisors in R; i.e., K is the fraction ring of R with respect to nonZeroDivisors(R).
Русский
Пусть R — коммутативное кольцо и K — коммутативное кольцо с алгебраическим отображением над R. Тогда K является локализацией R по множеству неприводимых делителей, то есть K — дробная локализация R.
LaTeX
$$$\text{IsFractionRing}(R,K) \equiv \text{IsLocalization}\big(\operatorname{nonZeroDivisors}(R), K\big)$$$
Lean4
/-- `IsFractionRing R K` states `K` is the ring of fractions of a commutative ring `R`. -/
abbrev IsFractionRing (R : Type*) [CommSemiring R] (K : Type*) [CommSemiring K] [Algebra R K] :=
IsLocalization (nonZeroDivisors R) K
