OAI/RingTheory/Multiplicity/CechCopies.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.FiniteModuleCech.copiesDiagram line 14
  2. def OAI.Lech.FiniteModuleCech.copiesDiagonal line 32
  3. def OAI.Lech.FiniteModuleCech.copiesProjection line 36
  4. lemma OAI.Lech.FiniteModuleCech.copies_positive_retract line 40
  5. def OAI.Lech.FiniteModuleCech.tensorCechMap line 46
  6. lemma OAI.Lech.FiniteModuleCech.copies_tensor_retract line 50
  7. lemma OAI.Lech.FiniteModuleCech.finite_of_copies line 59
  8. def OAI.Lech.FiniteModuleCech.copiesReindex line 69
  9. def OAI.Lech.FiniteModuleCech.copiesCongr line 78
  10. def OAI.Lech.FiniteModuleCech.copiesSuccEquiv line 82
  11. def OAI.Lech.FiniteModuleCech.copiesSuccIso line 91
  12. lemma OAI.Lech.FiniteModuleCech.copies_zero line 95
  13. lemma OAI.Lech.FiniteModuleCech.tensorEuler_copies_fin line 113
  14. lemma OAI.Lech.FiniteModuleCech.tensorEuler_copies line 142