OAI/RingTheory/Multiplicity/AlternatingCechPrismPrimitive.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.AlternatingCech.prismPrimitive line 29
  2. lemma OAI.Lech.AlternatingCech.prismPrimitive_apply line 39
  3. lemma OAI.Lech.AlternatingCech.prism_reduction_identity line 46
  4. lemma OAI.Lech.AlternatingCech.prism_reduction_cycle line 71
  5. abbrev OAI.Lech.ProductSourceCover.CentralIndex line 85
  6. def OAI.Lech.ProductSourceCover.centralIndexEquiv line 86
  7. instance OAI.Lech.ProductSourceCover.centralIndexFintype line 92
  8. lemma OAI.Lech.ProductSourceCover.centralIndex_card line 94
  9. def OAI.Lech.ProductSourceCover.centralModule line 107
  10. def OAI.Lech.ProductSourceCover.centralBasis line 109
  11. instance OAI.Lech.ProductSourceCover.centralModule_finite line 111
  12. instance OAI.Lech.ProductSourceCover.centralModule_free line 113
  13. lemma OAI.Lech.ProductSourceCover.centralModule_finrank line 115
  14. lemma OAI.Lech.ProductSourceCover.centralProjector_mem_central line 118
  15. def OAI.Lech.ProductSourceCover.centralCochain line 131
  16. lemma OAI.Lech.ProductSourceCover.centralCochain_val line 140
  17. theorem OAI.Lech.ProductSourceCover.central_cycle_representative line 145
  18. def OAI.Lech.ProductSourceCover.spanning line 174
  19. lemma OAI.Lech.ProductSourceCover.central_allowed_iff line 176
  20. def OAI.Lech.ProductSourceCover.centralSections line 211
  21. lemma OAI.Lech.ProductSourceCover.centralSections_mono line 213
  22. lemma OAI.Lech.ProductSourceCover.centralSections_eq line 217
  23. lemma OAI.Lech.ProductSourceCover.centralProjector_eq_self line 242
  24. theorem OAI.Lech.ProductSourceCover.central_exact_iff line 257
  25. def OAI.Lech.ProductSourceCover.exponentCons line 297
  26. lemma OAI.Lech.ProductSourceCover.exponentCons_zero line 299
  27. lemma OAI.Lech.ProductSourceCover.exponentCons_succ line 300
  28. lemma OAI.Lech.ProductSourceCover.exponentCons_injective line 302
  29. def OAI.Lech.ProductSourceCover.exponentTail line 306
  30. lemma OAI.Lech.ProductSourceCover.exponentTail_apply line 308
  31. lemma OAI.Lech.ProductSourceCover.exponentCons_tail line 309
  32. def OAI.Lech.ProductSourceCover.exponentSlice line 314
  33. def OAI.Lech.ProductSourceCover.exponentInsert line 316
  34. lemma OAI.Lech.ProductSourceCover.exponentSlice_apply line 318
  35. lemma OAI.Lech.ProductSourceCover.exponentSlice_insert line 320
  36. lemma OAI.Lech.ProductSourceCover.exponentInsert_support line 324
  37. def OAI.Lech.ProductSourceCover.trueFace line 328
  38. lemma OAI.Lech.ProductSourceCover.trueFace_injective line 329
  39. lemma OAI.Lech.ProductSourceCover.trueFace_zero line 333
  40. lemma OAI.Lech.ProductSourceCover.trueFace_succ line 334
  41. lemma OAI.Lech.ProductSourceCover.exponentSlice_mem line 335
  42. lemma OAI.Lech.ProductSourceCover.exponentInsert_mem line 354
  43. lemma OAI.Lech.ProductSourceCover.neighbor_mem_iff line 383
  44. lemma OAI.Lech.ProductSourceCover.neighbor_sections_le line 408
  45. def OAI.Lech.ProductSourceCover.faceVertexMap line 423
  46. lemma OAI.Lech.ProductSourceCover.faceVertexMap_basis line 425
  47. def OAI.Lech.ProductSourceCover.faceProjection line 427
  48. lemma OAI.Lech.ProductSourceCover.faceProjection_basis line 429
  49. def OAI.Lech.ProductSourceCover.faceSlice line 432
  50. lemma OAI.Lech.ProductSourceCover.faceSlice_eval line 437
  51. lemma OAI.Lech.ProductSourceCover.faceSlice_delta line 443
  52. def OAI.Lech.ProductSourceCover.faceLift line 454
  53. lemma OAI.Lech.ProductSourceCover.faceLift_eval line 459
  54. lemma OAI.Lech.ProductSourceCover.faceLift_eval_zero line 466
  55. lemma OAI.Lech.ProductSourceCover.faceSlice_lift line 473
  56. lemma OAI.Lech.ProductSourceCover.faceSlice_mem line 479
  57. lemma OAI.Lech.ProductSourceCover.faceLift_mem line 489