Finite_Integral_Domain_is_Galois_Field
Provedfinite-integral-domain-is-galois-fieldgalois-fieldsintegral-domainsproofwiki
A finite integral domain is a Galois field.
Preamble
import Mathlib.Algebra.Ring.Basic import Mathlib.RingTheory.Int.Basic import Mathlib.Data.Fintype.Card
Formal statement
theorem Finite_Integral_Domain_is_Galois_Field {R : Type _} [CommRing R] [IsDomain R] [Fintype R] : IsField R := by sorrySource