OAI/RingTheory/Multiplicity/LechConnectingIso.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.connecting_isoModSerre line 20
  2. def OAI.Lech.BicomplexTotal.positiveRows line 42
  3. lemma OAI.Lech.BicomplexTotal.positiveRows_bounded line 44
  4. lemma OAI.Lech.BicomplexTotal.positiveRows_acyclic line 51
  5. lemma OAI.Lech.BicomplexTotal.positiveRows_total_acyclic line 60
  6. lemma OAI.Lech.BicomplexTotal.bottom_total_shortExact line 66
  7. lemma OAI.Lech.BicomplexTotal.bottom_total_homology_isIso line 72
  8. def OAI.Lech.BicomplexTotal.bottomHomologyIso line 86
  9. def OAI.Lech.BicomplexTotal.doubleCoverIso line 94
  10. abbrev OAI.Lech.ComplexExtension.NatDouble line 108
  11. def OAI.Lech.ComplexExtension.doubleExtend line 111
  12. def OAI.Lech.ComplexExtension.rowIso line 114
  13. def OAI.Lech.ComplexExtension.columnEvalIso line 117
  14. def OAI.Lech.ComplexExtension.columnIso line 127
  15. lemma OAI.Lech.ComplexExtension.row_negative line 130
  16. lemma OAI.Lech.ComplexExtension.column_negative line 136
  17. lemma OAI.Lech.ComplexExtension.extended_acyclic line 143
  18. lemma OAI.Lech.ComplexExtension.row_bounded line 157
  19. lemma OAI.Lech.ComplexExtension.column_bounded line 164
  20. lemma OAI.Lech.ComplexExtension.row_positive line 171
  21. lemma OAI.Lech.ComplexExtension.column_positive line 176
  22. def OAI.Lech.ComplexExtension.natDoubleCoverIso line 182
  23. def OAI.Lech.AlternatingCech.sortedComplex line 200
  24. lemma OAI.Lech.AlternatingCech.sortedComplex_d line 206
  25. def OAI.Lech.AlternatingCech.cochainsSortedIso line 213
  26. lemma OAI.Lech.AlternatingCech.sortedDelta_injective line 224
  27. lemma OAI.Lech.AlternatingCech.sortedComplex_acyclic line 234
  28. lemma OAI.Lech.AlternatingCech.sortedComplex_bounded line 237
  29. lemma OAI.Lech.DoubleCech.row_exact line 257
  30. lemma OAI.Lech.DoubleCech.complex_d line 306
  31. def OAI.Lech.DoubleCech.switch line 309
  32. def OAI.Lech.DoubleCech.columnIso line 317
  33. lemma OAI.Lech.DoubleCech.row_bounded line 330
  34. lemma OAI.Lech.DoubleCech.column_bounded line 336
  35. def OAI.Lech.DoubleCech.coverComparison line 340
  36. def OAI.Lech.DoubleCech.emptyIndex line 364
  37. lemma OAI.Lech.DoubleCech.zeroIndex_eq line 366
  38. def OAI.Lech.DoubleCech.rowZeroEquiv line 371
  39. def OAI.Lech.DoubleCech.rowZeroIso line 378
  40. def OAI.Lech.DoubleCech.columnZeroIso line 388
  41. def OAI.Lech.AlternatingCech.zeroAugmentation line 400
  42. lemma OAI.Lech.AlternatingCech.zeroAugmentation_mono line 402
  43. def OAI.Lech.DoubleCech.puncture line 421
  44. lemma OAI.Lech.DoubleCech.puncture_left_mono line 425
  45. lemma OAI.Lech.DoubleCech.puncture_right_mono line 435
  46. lemma OAI.Lech.DoubleCech.puncture_row line 444
  47. lemma OAI.Lech.DoubleCech.puncture_column line 448
  48. def OAI.Lech.DoubleCech.unaugmentedCoverComparison line 454