OAI/Topology/ArtinGroups/Functors/LeftHomIndex.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.LeftHomIndex line 19
2. abbrev OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.RightHomIndex line 21
3. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.leftHomMatrix line 24
4. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.rightHomMatrix line 31
5. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.homSwitch line 40
6. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.homUnswitch line 45
7. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.homSwitch_inverse line 50
8. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.homUnswitch_inverse line 63
9. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.homSwitch_naturality line 76
10. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.homUnswitch_naturality line 104