FractionRing — Mathlib

English

The fraction ring of a domain is a field.

Русский

Дробная локализация домена образует поле.

LaTeX

$$FractionRing.field A$$

Lean4

/-- The fraction ring of a commutative ring `R` as a quotient type.

We instantiate this definition as generally as possible, and assume that the
commutative ring `R` is an integral domain only when this is needed for proving.

In this generality, this construction is also known as the *total fraction ring* of `R`.
-/
abbrev FractionRing :=
  Localization (nonZeroDivisors R)

Похожие утверждения