OAI/Topology/ArtinGroups/Harmonic/LayerExpression.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.HarmonicArtin.LayerExpression line 10
2. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.expressionAction line 30
3. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.expressionAction_sum line 37
4. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.classLabel_expression line 54
5. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.classLabel_expressionOrbit line 68
6. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.expressionOrbit_count_adjacency line 74
7. theorem OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.expressionOrbit_count_proportional line 87
8. theorem OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.string_expressionOrbit_count_proportional line 112