OAI/GroupTheory/FiniteType/OrderChainsExactInOfTop.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.OrderChains.exactIn_of_top line 19
2. def OAI.OrderBasedComplex.chosenBasis line 32
3. def OAI.OrderBasedComplex.chosenExtend line 41
4. lemma OAI.OrderBasedComplex.chosen_vertex line 44
5. lemma OAI.OrderBasedComplex.chosen_positive line 48
6. lemma OAI.OrderBasedComplex.chosen_spec line 67
7. def OAI.OrderBasedComplex.chosenHomotopyBasis line 126
8. def OAI.OrderBasedComplex.chosenHomotopy line 134
9. lemma OAI.OrderBasedComplex.chosenHomotopy_equation line 136
10. lemma OAI.OrderBasedComplex.chosenHomotopy_spec line 161
11. lemma OAI.OrderListChains.augmentation_of_positive line 225
12. lemma OAI.OrderListChains.mapChain_eq_on line 234