OAI/RingTheory/BassTrace/TreeDeterminants.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

An oriented incidence matrix of a tree, with its root row deleted, is unimodular, independently of a planar structure or ordering of children.

  1. def OAI.BassTrace.Sparse.treeEdgeEquiv line 14
  2. def OAI.BassTrace.Sparse.rootCoordinate line 23
  3. lemma OAI.BassTrace.Sparse.rootCoordinate_zero line 26
  4. lemma OAI.BassTrace.Sparse.rootCoordinate_succ line 30
  5. def OAI.BassTrace.Sparse.treeIncidence line 35
  6. lemma OAI.BassTrace.Sparse.adjacent_difference_mem_span line 40
  7. lemma OAI.BassTrace.Sparse.walk_difference_mem_span line 63
  8. lemma OAI.BassTrace.Sparse.treeIncidence_span line 74
  9. theorem OAI.BassTrace.Sparse.treeIncidence_isUnit_det line 90
  10. theorem OAI.BassTrace.Sparse.treeIncidence_abs_real_det line 98
  11. def OAI.BassTrace.Sparse.realTreeIncidence line 107
  12. lemma OAI.BassTrace.Sparse.realTreeIncidence_det_ne_zero line 111
  13. theorem OAI.BassTrace.Sparse.treeChart_measurePreserving line 119
  14. def OAI.BassTrace.Sparse.treeGradient line 127
  15. lemma OAI.BassTrace.Sparse.treeGradient_norm_le_one line 133
  16. lemma OAI.BassTrace.Sparse.rootCoordinate_potential line 161
  17. lemma OAI.BassTrace.Sparse.treeChart_potential line 167
  18. def OAI.BassTrace.Sparse.treeSolidSimplex line 195
  19. lemma OAI.BassTrace.Sparse.treeSolidSimplex_volume line 199
  20. def OAI.BassTrace.Sparse.barycentricParam line 214
  21. lemma OAI.BassTrace.Sparse.barycentricParam_zero line 217
  22. lemma OAI.BassTrace.Sparse.barycentricParam_succ line 220
  23. lemma OAI.BassTrace.Sparse.sum_barycentricParam line 223
  24. lemma OAI.BassTrace.Sparse.barycentricParam_injective line 228
  25. lemma OAI.BassTrace.Sparse.range_barycentricParam line 234
  26. lemma OAI.BassTrace.Sparse.continuous_barycentricParam line 251
  27. def OAI.BassTrace.Sparse.treeParam line 258
  28. lemma OAI.BassTrace.Sparse.treeParam_injective line 262
  29. lemma OAI.BassTrace.Sparse.range_treeParam line 270
  30. lemma OAI.BassTrace.Sparse.continuous_treeParam line 280
  31. def OAI.BassTrace.Sparse.treeArea line 285
  32. lemma OAI.BassTrace.Sparse.treeArea_mono line 289
  33. lemma OAI.BassTrace.Sparse.treeArea_union line 293
  34. def OAI.BassTrace.Sparse.fullBarycentricSimplex line 298
  35. lemma OAI.BassTrace.Sparse.barycentricParam_mem_simplex line 301
  36. lemma OAI.BassTrace.Sparse.treeArea_top_simplex line 312
  37. lemma OAI.BassTrace.Sparse.hausdorff_zero_eq_count line 324
  38. lemma OAI.BassTrace.Sparse.treeArea_zero line 341
  39. def OAI.BassTrace.Sparse.SpanningTree line 348
  40. instance OAI.BassTrace.Sparse.(instance at line 351) line 351
  41. lemma OAI.BassTrace.Sparse.nonempty_spanningTree line 356
  42. def OAI.BassTrace.Sparse.simplexArea line 361
  43. lemma OAI.BassTrace.Sparse.simplexArea_mono line 365
  44. lemma OAI.BassTrace.Sparse.simplexArea_top_simplex line 371
  45. lemma OAI.BassTrace.Sparse.simplexArea_zero line 377