Field_is_Integral_Domain
Provedfieldsintegral-domainsproofwiki
Every field is an integral domain.
Preamble
import Mathlib.Algebra.Field.Basic
Formal statement
theorem Field_is_Integral_Domain {F : Type _} [Field F] : IsDomain F := by sorrySource
Every field is an integral domain.
import Mathlib.Algebra.Field.Basic
theorem Field_is_Integral_Domain {F : Type _} [Field F] : IsDomain F := by sorry