OAI/RingTheory/BassTrace/TreeArea.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BassTrace.Sparse.treeMatrixEquiv line 15
  2. def OAI.BassTrace.Sparse.independentCoordinates line 23
  3. def OAI.BassTrace.Sparse.treeCoordinates line 28
  4. lemma OAI.BassTrace.Sparse.treeCoordinates_treeParam line 33
  5. lemma OAI.BassTrace.Sparse.treeParam_treeCoordinates line 39
  6. lemma OAI.BassTrace.Sparse.treeParam_preimage_eq_image line 44
  7. lemma OAI.BassTrace.Sparse.convex_sum_one line 54
  8. lemma OAI.BassTrace.Sparse.treeParam_preimage_simplex line 63
  9. lemma OAI.BassTrace.Sparse.euclideanArea_eq_zero_of_dimH_lt line 76
  10. lemma OAI.BassTrace.Sparse.euclideanArea_simplex_eq_zero line 83
  11. lemma OAI.BassTrace.Sparse.euclideanArea_simplex_lt_top line 105
  12. lemma OAI.BassTrace.Sparse.treeArea_simplex_lt_top line 150
  13. lemma OAI.BassTrace.Sparse.treeArea_simplex_eq_zero line 160
  14. lemma OAI.BassTrace.Sparse.simplexArea_simplex_lt_top line 170
  15. lemma OAI.BassTrace.Sparse.simplexArea_simplex_eq_zero line 181
  16. lemma OAI.BassTrace.Sparse.treeArea_iUnion_le line 189
  17. lemma OAI.BassTrace.Sparse.treeArea_polyhedral_lt_top line 195
  18. lemma OAI.BassTrace.Sparse.simplexArea_polyhedral_lt_top line 204