OAI/RingTheory/Multiplicity/ProductSourceCoverHighThreshold.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.ProductSourceCover.highThreshold line 22
  2. lemma OAI.Lech.ProductSourceCover.level_high line 23
  3. def OAI.Lech.ProductSourceCover.fraction line 34
  4. lemma OAI.Lech.ProductSourceCover.fraction_spec line 36
  5. lemma OAI.Lech.ProductSourceCover.uniform_witness line 42
  6. lemma OAI.Lech.ProductSourceCover.grid_source_exact line 61
  7. theorem OAI.Lech.ProductSourceCover.grid_source_acyclic line 108
  8. lemma OAI.Lech.AlternatingCech.scalar_uniform_clear line 143
  9. theorem OAI.Lech.AlternatingCech.scalar_exact line 156
  10. lemma OAI.Lech.AlternatingCech.scalar_complex_acyclic line 183
  11. lemma OAI.Lech.ProductLinearChart.linear_content_top line 205
  12. lemma OAI.Lech.ProductLinearChart.product_content_top line 213
  13. lemma OAI.Lech.ProductLinearChart.coefficients_span line 223
  14. lemma OAI.Lech.ProductSourceCover.monomialUnit_sum line 243
  15. lemma OAI.Lech.ProductSourceCover.chartUnit_monomial line 249
  16. lemma OAI.Lech.ProductSourceCover.chartUnit_inv_section line 267
  17. lemma OAI.Lech.ProductSourceCover.chartMap_zero_section line 275
  18. def OAI.Lech.ProductSourceCover.chartScalar line 283
  19. lemma OAI.Lech.ProductSourceCover.grid_chart_stable line 285
  20. lemma OAI.Lech.ProductSourceCover.grid_target_clear line 294
  21. theorem OAI.Lech.ProductSourceCover.grid_target_acyclic line 324
  22. abbrev OAI.Lech.ProductSourceCover.gridComplex line 344
  23. def OAI.Lech.ProductSourceCover.grid_homology_comparison line 348
  24. lemma OAI.Lech.ProductSourceCover.grid_empty_target line 362
  25. def OAI.Lech.ProductSourceCover.gridSourceEdgeIso line 379
  26. def OAI.Lech.ProductSourceCover.sourceSectionComplex line 392
  27. def OAI.Lech.ProductSourceCover.targetSectionComplex line 394
  28. def OAI.Lech.ProductSourceCover.sectionCohomologyComparison line 398
  29. def OAI.Lech.ProductSourceCover.sourceCech line 419
  30. def OAI.Lech.ProductSourceCover.targetCech line 422
  31. def OAI.Lech.ProductSourceCover.gridSourceUnaugmentedIso line 424
  32. def OAI.Lech.ProductSourceCover.gridUnaugmentedComparison line 429
  33. def OAI.Lech.ProductSourceCover.cechCohomologyComparison line 438