OAI/Topology/ArtinGroups/Functors/Evaluation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.pathImage_single line 19
2. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.image_coordinate_base_ne line 49
3. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.evaluationSource line 60
4. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.evaluationTarget line 62
5. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.evaluationMatrix line 65
6. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.evaluationMatrix_sector line 72
7. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.evaluationMatrix_vecMul line 104
8. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.evaluationMatrix_bijective line 126
9. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearMap_mul_corner line 139
10. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.evaluation_naturality line 159