OAI/RingTheory/BassTrace/FundamentalChains.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.Sparse.sum_real_sign line 20
  2. lemma OAI.BassTrace.Sparse.signed_facet_incidence line 32
  3. lemma OAI.BassTrace.Sparse.one_sided_parent_unique line 49
  4. lemma OAI.BassTrace.Sparse.parent_boundary_sign_sum line 87
  5. lemma OAI.BassTrace.Sparse.signed_facet_boundary line 157
  6. def OAI.BassTrace.Fundamental.faces line 183
  7. lemma OAI.BassTrace.Fundamental.mem_faces line 189
  8. lemma OAI.BassTrace.Fundamental.apexes_faces line 194
  9. theorem OAI.BassTrace.Fundamental.geometric_boundary_coefficient line 214
  10. lemma OAI.BassTrace.Fundamental.sum_vertices line 237
  11. lemma OAI.BassTrace.Fundamental.chain_coefficient line 245
  12. lemma OAI.BassTrace.Fundamental.boundary_coefficient_nonface line 257
  13. def OAI.BassTrace.Fundamental.faceChain line 275
  14. lemma OAI.BassTrace.Fundamental.faceChain_coefficient line 283
  15. lemma OAI.BassTrace.Fundamental.forall_vertices_except line 310
  16. theorem OAI.BassTrace.Fundamental.boundary_chain line 325
  17. lemma OAI.BassTrace.Fundamental.sum_enumeration line 351
  18. lemma OAI.BassTrace.Fundamental.forall_enumeration_except line 360
  19. theorem OAI.BassTrace.Fundamental.boundary_chain_chart line 370
  20. def OAI.BassTrace.Fundamental.term line 407
  21. lemma OAI.BassTrace.Fundamental.term_perm line 410
  22. lemma OAI.BassTrace.Fundamental.parent_face_chart line 432