OAI/RingTheory/Kurosh/Ultraproduct.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Division-ring ultraproducts and equality of representatives.

  1. def OAI.KuroshConstruction.ultraCongruence line 13
  2. abbrev OAI.KuroshConstruction.DivisionUltraproduct line 21
  3. def OAI.KuroshConstruction.ultraMap line 23
  4. lemma OAI.KuroshConstruction.ultraMap_eq_iff line 26
  5. instance OAI.KuroshConstruction.divisionUltraproduct_nontrivial line 30
  6. instance OAI.KuroshConstruction.divisionUltraproductDivisionRing line 38
  7. instance OAI.KuroshConstruction.(instance at line 62) line 62