OAI/Topology/ArtinGroups/Complexes/Identity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.identity line 20
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.comp line 27
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.conjugateBoundary line 35
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomotopyEquivalence.refl line 51
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomotopyEquivalence.trans line 69
6. structure OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.FiniteModel line 132
7. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.FiniteModel.ofComplex line 142
8. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.FiniteModel.exists_minimal line 149