OAI/RingTheory/BassTrace/SubdivisionWeights.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BassTrace.Sparse.generatedComplex line 19
  2. lemma OAI.BassTrace.Sparse.generatedComplex_invariant line 28
  3. lemma OAI.BassTrace.Sparse.generatedComplex_top_mem line 37
  4. lemma OAI.BassTrace.Sparse.connected_smul line 41
  5. lemma OAI.BassTrace.Sparse.generatedComplex_pure line 53
  6. def OAI.BassTrace.Sparse.generatedReps line 63
  7. lemma OAI.BassTrace.Sparse.generatedReps_mem line 66
  8. lemma OAI.BassTrace.Sparse.generatedReps_complete line 72
  9. lemma OAI.BassTrace.Sparse.generatedTop_finite line 84
  10. def OAI.BassTrace.Sparse.uniformVector line 114
  11. lemma OAI.BassTrace.Sparse.uniformVector_apply line 117
  12. lemma OAI.BassTrace.Sparse.uniformVector_sum line 122
  13. lemma OAI.BassTrace.Sparse.uniformVector_nat line 128
  14. lemma OAI.BassTrace.Sparse.supportVertices_push line 135
  15. def OAI.BassTrace.Sparse.componentVertices line 163
  16. lemma OAI.BassTrace.Sparse.mem_componentVertices line 166
  17. lemma OAI.BassTrace.Sparse.componentVertices_nonempty line 170
  18. lemma OAI.BassTrace.Sparse.componentVertices_nat line 175
  19. def OAI.BassTrace.Sparse.componentWeight line 183
  20. lemma OAI.BassTrace.Sparse.componentWeight_sum line 186
  21. lemma OAI.BassTrace.Sparse.componentWeight_nat line 190
  22. lemma OAI.BassTrace.Sparse.componentWeight_eq_of_component line 196
  23. lemma OAI.BassTrace.Sparse.componentWeight_support line 205
  24. def OAI.BassTrace.Sparse.faceWeight line 238
  25. lemma OAI.BassTrace.Sparse.faceWeight_sum line 243
  26. lemma OAI.BassTrace.Sparse.faceWeight_face line 250
  27. lemma OAI.BassTrace.Sparse.faceWeight_nat line 257
  28. lemma OAI.BassTrace.Sparse.faceWeight_nested_equal_level line 264
  29. lemma OAI.BassTrace.Sparse.faceWeight_local line 271
  30. def OAI.BassTrace.SubdivisionChains.chart line 308
  31. lemma OAI.BassTrace.SubdivisionChains.chart_apply line 312
  32. lemma OAI.BassTrace.SubdivisionChains.chart_vertex line 316
  33. def OAI.BassTrace.SubdivisionChains.localTriangulation line 321
  34. lemma OAI.BassTrace.SubdivisionChains.localTriangulation_finite line 325
  35. lemma OAI.BassTrace.SubdivisionChains.localTriangulation_space line 329
  36. def OAI.BassTrace.SubdivisionChains.tupleSubdivision line 336
  37. lemma OAI.BassTrace.SubdivisionChains.chain_chart_perm line 343
  38. lemma OAI.BassTrace.SubdivisionChains.tupleSubdivision_perm line 361
  39. lemma OAI.BassTrace.SubdivisionChains.tupleSubdivision_zero line 370
  40. def OAI.BassTrace.SubdivisionChains.subdivisionValues line 383
  41. def OAI.BassTrace.SubdivisionChains.subdivision line 388
  42. lemma OAI.BassTrace.SubdivisionChains.subdivision_wedge_succ line 392
  43. lemma OAI.BassTrace.SubdivisionChains.subdivision_wedge_face line 396
  44. lemma OAI.BassTrace.SubdivisionChains.simplexVertices_image line 418
  45. lemma OAI.BassTrace.SubdivisionChains.localTriangulation_face line 431
  46. lemma OAI.BassTrace.SubdivisionChains.subdivision_chain_wedge line 448