OAI/Topology/ArtinGroups/Functors/SectorInverse.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.sectorInverse line 16
2. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.inverseEvaluationMatrix line 22
3. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.inverseEvaluationMatrix_sector line 30
4. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.linearSwitch_symm_sector line 41
5. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.inverseEvaluationMatrix_vecMul line 60
6. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.evaluationMatrix_inverse line 82
7. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.inverseEvaluationMatrix_inverse line 97
8. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.evaluationMatrix_length line 112
9. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.inverseEvaluationMatrix_length line 123