Zero_of_Inverse_Completion_of_Integral_Domain
Provedintegral-domainsinverse-completionsproofwiki
Let (D, +, *) be an integral domain. Let K be its field of fractions. Then the zero of D maps to the zero of K.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.RingTheory.Localization.FractionRing
Formal statement
theorem Zero_of_Inverse_Completion_of_Integral_Domain {D : Type _} [CommRing D] [IsDomain D] (K : Type _) [Field K] [Algebra D K] [IsFractionRing D K] : (algebraMap D K) 0 = 0 := by sorrySource