OAI/RingTheory/Kurosh/AlgebraicClosure.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Algebraicity, inverse closure, and countability of generated algebras.

  1. def OAI.KuroshConstruction.RelationsScheduled line 21
  2. theorem OAI.KuroshConstruction.scheduled_isIntegral line 26
  3. def OAI.KuroshConstruction.scheduledDivisionRing line 44
  4. theorem OAI.KuroshConstruction.countable_generated_algebra line 61