Field_of_Quotients_is_Unique

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Field_of_Quotients_is_Unique is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Let $\struct {D, +, \circ}$ be an integral domain. Let $K, L$ be field of quotients of $\struct {D, +, \circ}$. Then there is one and only one (field) isomorphism $\phi: K \to L$ satisfying $\forall x \in D: \map \phi x = x$

Why this node was retired

The posted statement is

theorem Field_of_Quotients_is_Unique (D : Type _) [CommRing D] [IsDomain D] : ∃ f : FractionRing D ≃+* FractionRing D, True := by sorry

The goal is ∃ f : FractionRing D ≃+* FractionRing D, True, witnessed by the identity. It relates FractionRing D to itself rather than to an arbitrary field of quotients of D, so no uniqueness is asserted.

What a faithful statement would require

The statement must quantify over an arbitrary field K with an embedding of D satisfying the universal property, and conclude that K ≃+* FractionRing D over D.

No corrected replacement node exists yet.