OAI/Topology/ArtinGroups/Functors/Index.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearMap_apply line 21
  2. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearMap_left line 26
  3. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearMap_right line 33
  4. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.pathImage_homogeneous line 40
  5. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearMap_homogeneous line 60
  6. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearMap_support line 73
  7. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearMap_positive line 84
  8. abbrev OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.Index line 99
  9. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.indexEmbed line 102
  10. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.placement line 105
  11. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.matrix line 109
  12. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.matrix_zero line 114
  13. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.matrix_add line 121
  14. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.matrix_smul line 129
  15. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.matrix_entries line 137
  16. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.matrix_degree line 147
  17. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.matrix_mul line 160
  18. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.matrix_identity line 191
  19. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.complex line 218
  20. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.complex_minimal line 234
  21. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.map line 255
  22. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.map_comp line 267
  23. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.map_identity line 277
  24. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.homotopyEquivalence line 283