OAI/Topology/ArtinGroups/Functors/LeftHomPlacement.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.leftHomPlacement line 17
2. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.rightHomEquiv line 21
3. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.rightHomPlacement line 28
4. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.rightHomMatrix_eq line 32
5. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.leftHom_degree line 39
6. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.rightHomComplex line 69
7. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.rightHomMatrix_square line 75
8. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.leftHomMatrix_square line 88
9. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.leftHomComplex line 108