OAI/RingTheory/Kurosh/LimitScalars.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compatible tail-field maps and the limiting scalar field.

  1. def OAI.KuroshConstruction.tailCoefficients line 21
  2. def OAI.KuroshConstruction.ultraStageMap line 24
  3. lemma OAI.KuroshConstruction.ultraStageMap_compatible line 46
  4. def OAI.KuroshConstruction.ultraLimitMap line 53
  5. lemma OAI.KuroshConstruction.ultraStageMap_commutes line 58
  6. lemma OAI.KuroshConstruction.ultraLimitMap_commutes line 69
  7. def OAI.KuroshConstruction.ultraLimitAlgebra line 74