OAI/Topology/ArtinGroups/Harmonic/FusionLabel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.FusionLabel line 10
2. def OAI.HarmonicArtin.fusionWeight line 12
3. lemma OAI.HarmonicArtin.fusionWeight_pos line 16
4. def OAI.HarmonicArtin.factorMultiplicity line 22
5. lemma OAI.HarmonicArtin.factorMultiplicity_symm line 25
6. lemma OAI.HarmonicArtin.factorMultiplicity_le_one line 32
7. lemma OAI.HarmonicArtin.fusionWeight_update line 39
8. lemma OAI.HarmonicArtin.factorMultiplicity_update line 50
9. lemma OAI.HarmonicArtin.factor_dimension_identity line 59
10. inductive OAI.HarmonicArtin.FusionEdge line 90
11. def OAI.HarmonicArtin.FusionEdge.multiplicity line 94
12. def OAI.HarmonicArtin.FusionEdge.dimension line 99
13. lemma OAI.HarmonicArtin.FusionEdge.multiplicity_symm line 104
14. lemma OAI.HarmonicArtin.FusionEdge.dimension_identity line 110