OAI/RingTheory/Multiplicity/ArbitraryCoefficientField.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.ArbitraryCoefficientField.power_strictMono line 11
  2. lemma OAI.Lech.ArbitraryCoefficientField.transition_ker line 15
  3. lemma OAI.Lech.ArbitraryCoefficientField.exists_next line 21
  4. def OAI.Lech.ArbitraryCoefficientField.stage line 33
  5. lemma OAI.Lech.ArbitraryCoefficientField.stage_compatible line 37
  6. def OAI.Lech.ArbitraryCoefficientField.sectionMap line 44
  7. lemma OAI.Lech.ArbitraryCoefficientField.sectionMap_mod line 48
  8. def OAI.Lech.ArbitraryCoefficientField.quotientSectionData line 65
  9. def OAI.Lech.ArbitraryCoefficientField.localSection line 76
  10. lemma OAI.Lech.ArbitraryCoefficientField.localSection_rightInverse line 78
  11. lemma OAI.Lech.ArbitraryCoefficientField.localSection_injective line 82