OAI/GroupTheory/FiniteType/HornElimination.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HornElimination.earlyFace line 28
  2. abbrev OAI.HornElimination.pivotFace line 29
  3. def OAI.HornElimination.pivotFamily line 31
  4. def OAI.HornElimination.pivot line 36
  5. lemma OAI.HornElimination.pivot_early line 39
  6. lemma OAI.HornElimination.pivot_last line 52
  7. lemma OAI.HornElimination.pivot_double line 56
  8. def OAI.HornElimination.side line 59
  9. lemma OAI.HornElimination.side_last line 63
  10. lemma OAI.HornElimination.side_penult line 68
  11. lemma OAI.HornElimination.side_prepenult line 76
  12. lemma OAI.HornElimination.side_small line 85
  13. def OAI.HornElimination.family line 91
  14. lemma OAI.HornElimination.family_ordered line 95
  15. lemma OAI.HornElimination.family_compatible line 139
  16. def OAI.HornElimination.higher line 144
  17. lemma OAI.HornElimination.higher_face line 147
  18. lemma OAI.SimplexBoundary.face_ordered line 158
  19. lemma OAI.SimplexBoundary.face_comp_ordered line 167
  20. lemma OAI.SimplexBoundary.doubleBoundary_of_faces line 171
  21. def OAI.HornElimination.replacementFace line 189
  22. def OAI.HornElimination.replacement line 192
  23. lemma OAI.HornElimination.replacement_early line 195
  24. lemma OAI.HornElimination.replacement_pivot line 210
  25. lemma OAI.HornElimination.replacement_last line 222
  26. def OAI.HornElimination.newFaces line 228
  27. lemma OAI.HornElimination.replacement_faces line 232
  28. lemma OAI.HornElimination.replacement_double line 244
  29. lemma OAI.HornElimination.new_basedFace line 247