OAI/RingTheory/Kurosh/ScheduledLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The division ring obtained from a compatible scheduled tower.

  1. lemma OAI.KuroshConstruction.field_limit_countable line 14
  2. lemma OAI.KuroshConstruction.generated_adjoin_eq_top line 22
  3. def OAI.KuroshConstruction.MainStatement line 36
  4. theorem OAI.KuroshConstruction.scheduled_tower_yields_main line 45