OAI/RingTheory/Multiplicity/ScalarCechShift.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.FilteredCech.positiveXIso_d line 13
  2. lemma OAI.Lech.FilteredCech.complex_d line 26
  3. abbrev OAI.Lech.FilteredCech.shiftedPositive line 32
  4. abbrev OAI.Lech.FilteredCech.ordinaryPositive line 33
  5. def OAI.Lech.FilteredCech.shiftXIso line 35
  6. lemma OAI.Lech.FilteredCech.shiftXIso_d line 50
  7. def OAI.Lech.FilteredCech.shiftRestrictionIso line 72
  8. lemma OAI.Lech.FilteredCech.shiftRestriction_hasLift line 78
  9. def OAI.Lech.FilteredCech.shiftToOrdinary line 89
  10. instance OAI.Lech.FilteredCech.shiftToOrdinary_isIso line 93
  11. def OAI.Lech.FilteredCech.shiftOrdinaryIso line 103