OAI/RingTheory/Multiplicity/ReesRootNilpotence.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.ReesRoot.intersectionTensorHomotopy line 42
  2. def OAI.Lech.ReesRoot.intersectionCechHomotopy line 57
  3. def OAI.Lech.ReesRoot.cechNatTensorHomotopy line 72
  4. def OAI.Lech.ReesRoot.cechInclusionZ line 84
  5. def OAI.Lech.ReesRoot.cechZTensorHomotopy line 88
  6. def OAI.Lech.ReesRoot.enlargedAt line 111
  7. def OAI.Lech.ReesRoot.enlargedMap line 115
  8. def OAI.Lech.ReesRoot.enlargedRowHomotopy line 122
  9. lemma OAI.Lech.ReesRoot.enlargedAt_isZero line 129
  10. def OAI.Lech.ReesRoot.twistSequence line 138
  11. lemma OAI.Lech.ReesRoot.twistSequence_apply line 142
  12. def OAI.Lech.ReesRoot.enlargedStep line 151
  13. lemma OAI.Lech.ReesRoot.enlargedPath_homology_zero line 159
  14. theorem OAI.Lech.ReesRoot.uniform_enlarged_nilpotence line 173