Inverse_Completion_Less_Zero_of_Integral_Domain_is_Closed
Provedintegral-domainsinverse-completionsproofwiki
Let K be the field of fractions of an integral domain. Then K \ {0} is closed under multiplication.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Inverse_Completion_Less_Zero_of_Integral_Domain_is_Closed {K : Type _} [Field K] (a b : K) (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 := by sorrySource