OAI/RingTheory/Kurosh/LiftingStages.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compatible finite stages and the consequences of an algebraic lift.

  1. lemma OAI.KuroshConstruction.scalarChange_free_evaluate line 16
  2. lemma OAI.KuroshConstruction.scalarChange_series_evaluate line 26
  3. def OAI.KuroshConstruction.freeRename line 38
  4. lemma OAI.KuroshConstruction.freeRename_evaluate line 41
  5. structure OAI.KuroshConstruction.LiftingStage line 50
  6. structure OAI.KuroshConstruction.LiftingStep line 67
  7. theorem OAI.KuroshConstruction.lifting_step_exists line 75