OAI/RingTheory/BassTrace/Incidence.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BassTrace.OrientedIncidence.vertices line 19
  2. lemma OAI.BassTrace.OrientedIncidence.vertices_mem line 22
  3. lemma OAI.BassTrace.OrientedIncidence.vertices_range line 25
  4. def OAI.BassTrace.OrientedIncidence.eraseFace line 28
  5. lemma OAI.BassTrace.OrientedIncidence.eraseFace_val line 32
  6. lemma OAI.BassTrace.OrientedIncidence.vertices_eraseFace line 35
  7. lemma OAI.BassTrace.OrientedIncidence.boundary_basis line 43
  8. lemma OAI.BassTrace.OrientedIncidence.boundary_basis_coefficient line 53
  9. lemma OAI.BassTrace.OrientedIncidence.insert_eraseFace line 71
  10. lemma OAI.BassTrace.OrientedIncidence.eraseFace_neq line 75
  11. lemma OAI.BassTrace.OrientedIncidence.incidence_pair_injective line 78
  12. def OAI.BassTrace.OrientedIncidence.incidencePairs line 88
  13. def OAI.BassTrace.OrientedIncidence.apexes line 92
  14. lemma OAI.BassTrace.OrientedIncidence.mem_apexes line 95
  15. lemma OAI.BassTrace.OrientedIncidence.sum_incidencePairs line 112
  16. lemma OAI.BassTrace.OrientedIncidence.boundary_sum_coefficient line 120
  17. lemma OAI.BassTrace.Sparse.Orientation.linearIndependent_of_normalized line 143
  18. lemma OAI.BassTrace.Sparse.Orientation.det_ne_zero_of_normalized line 154
  19. def OAI.BassTrace.Sparse.Orientation.facetForm line 160
  20. lemma OAI.BassTrace.Sparse.Orientation.facetForm_apply line 165
  21. lemma OAI.BassTrace.Sparse.Orientation.facetForm_vertex line 168
  22. lemma OAI.BassTrace.Sparse.Orientation.facetForm_convexHull line 174
  23. lemma OAI.BassTrace.Sparse.Orientation.det_cons_delete line 183
  24. lemma OAI.BassTrace.Sparse.Orientation.realSign_negOnePow_mul line 192
  25. lemma OAI.BassTrace.Sparse.Orientation.determinant_deletion_orientation line 199
  26. lemma OAI.BassTrace.Sparse.Orientation.det_cons_unit line 209
  27. lemma OAI.BassTrace.Sparse.Orientation.facetForm_on_unit line 229
  28. lemma OAI.BassTrace.Sparse.Orientation.facetForm_column_zero line 234
  29. lemma OAI.BassTrace.Sparse.Orientation.linearMap_eq_coord_of_units line 244
  30. lemma OAI.BassTrace.Sparse.Orientation.facet_boundary_term line 258
  31. def OAI.BassTrace.Fundamental.chain line 288
  32. lemma OAI.BassTrace.Fundamental.boundary_coefficient line 292