Field_of_Characteristic_Zero_has_Unique_Prime_Subfield
Provedcharacteristicfield-theoryprime-subfieldproofwiki
Let be a field, whose zero is and whose unity is , with characteristic zero. Then there exists a unique such that is a subfield of is isomorphic to the field of rational numbers . That is, is a unique minimal subfield of , and all other subfields of contain . This field is called the prime subfield of .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Field_of_Characteristic_Zero_has_Unique_Prime_Subfield {F : Type _} [Field F] [CharZero F] : Nonempty (ℚ →+* F) := by sorrySource