OAI/RingTheory/Multiplicity/SourceGradedCechHomology.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.component_iso_square line 10

    Distinct definitions of this name: OAI/RingTheory/Multiplicity/FilteredCechAugmented.lean:10 (same statement text; different proof or body). Qualify references as OAI.component_iso_square@path.

  2. theorem OAI.Lech.SourceGraded.cech_homology_value line 36
  3. def OAI.Lech.SignedFraction.order line 105
  4. lemma OAI.Lech.SignedFraction.order_nat line 107
  5. lemma OAI.Lech.SignedFraction.order_add_le line 110
  6. def OAI.Lech.SignedFraction.fraction line 118
  7. def OAI.Lech.SignedFraction.piece line 123
  8. lemma OAI.Lech.SignedFraction.fraction_mem line 126
  9. lemma OAI.Lech.SignedFraction.raise_fraction line 132
  10. lemma OAI.Lech.SignedFraction.range_mono line 147
  11. lemma OAI.Lech.SignedFraction.exists_fraction line 153
  12. lemma OAI.Lech.SignedFraction.antitone line 161
  13. lemma OAI.Lech.SignedFraction.piece_nat line 177
  14. lemma OAI.Lech.SignedFraction.order_divide_le line 191
  15. lemma OAI.Lech.SignedFraction.inverseFactor_fraction line 202
  16. lemma OAI.Lech.SignedFraction.inverseFactor_mem line 222
  17. def OAI.Lech.SignedFraction.divide line 231
  18. lemma OAI.Lech.SignedFraction.smul_divide line 238
  19. lemma OAI.Lech.SignedFraction.order_restrict_le line 254
  20. lemma OAI.Lech.SignedFraction.restriction_fraction line 264
  21. lemma OAI.Lech.SignedFraction.restriction_mem line 277
  22. abbrev OAI.Lech.SignedCech.term line 294
  23. lemma OAI.Lech.SignedCech.restriction_mem line 299
  24. def OAI.Lech.SignedCech.complex line 305
  25. def OAI.Lech.SignedCech.inclusion line 308
  26. lemma OAI.Lech.SignedCech.inclusion_refl line 311
  27. lemma OAI.Lech.SignedCech.inclusion_comp line 315
  28. instance OAI.Lech.SignedCech.inclusion_mono line 320
  29. lemma OAI.Lech.SignedCech.term_nat line 327
  30. def OAI.Lech.SignedCech.augmented line 337
  31. lemma OAI.Lech.SignedCech.augmented_boundedBelow line 340
  32. def OAI.Lech.SignedCech.positive line 350
  33. lemma OAI.Lech.SignedCech.positive_boundedBelow line 353
  34. def OAI.Lech.SignedCech.positiveInclusion line 358
  35. def OAI.Lech.SignedCech.positiveXIso line 362
  36. lemma OAI.Lech.SignedCech.positiveXIso_inclusion line 367
  37. lemma OAI.Lech.SignedCech.positiveInclusion_refl line 381
  38. lemma OAI.Lech.SignedCech.positiveInclusion_comp line 395
  39. def OAI.Lech.SignedCech.divide line 425
  40. lemma OAI.Lech.SignedCech.smul_divide line 431
  41. def OAI.Lech.SignedCech.intersectionHomotopy line 452
  42. def OAI.Lech.SignedCech.cochainPiIso line 464
  43. lemma OAI.Lech.SignedCech.cochainPiIso_inclusion line 468
  44. def OAI.Lech.SignedCech.cochainHomotopy line 479
  45. def OAI.Lech.SignedCech.positiveRowHomotopy line 495