OAI/RingTheory/DirectFiniteness/FieldExtensions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KaplanskyCounterexample.FiniteGeometry.exists_finite_extension line 10

   Source documentation

   Finite characteristic-two fields have finite extensions of every positive degree.

   theorem exists_finite_extension (Q : Type) [Field Q] [Fintype Q] [CharP Q 2]
       (b : ℕ) (hb : 0 < b) :
       ∃ (F : Type) (_ : Field F) (_ : Algebra Q F) (_ : Fintype F),
         finrank Q F = b := by
   …