OAI/Topology/ArtinGroups/Functors/PathImage.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.arrowImage_mul_of_not_composable line 17
2. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.coefficient_square line 32
3. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.arrowImage_entry_product line 81
4. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.arrowImage_mul_arrowImage line 120
5. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.pathImage line 226
6. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearMap line 232
7. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearMap_pathBasis line 236
8. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.pathImage_left line 242
9. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.pathImage_right line 256
10. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.pathImage_support line 273
11. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.unitImage_pathImage line 291
12. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.pathImage_unitImage line 310
13. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.pathImage_positive line 330
14. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.tokenImage_pathImage line 344
15. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.pathImage_tokenImage line 358
16. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearMap_mul line 372