Existence_of_Field_of_Quotients

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

fields-of-quotientsintegral-domainsproofwiki

Let $\struct {D, +, \circ}$ be an integral domain. Then there exists a field of quotients of $\struct {D, +, \circ}$ .

Preamble

import Mathlib.RingTheory.Localization.FractionRing

Formal statement

theorem Existence_of_Field_of_Quotients (D : Type _) [CommRing D] [IsDomain D] : ∃ (_ : Field (FractionRing D)), True := by sorry

Source