OAI/Topology/ArtinGroups/Harmonic/FusionRest.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.FusionRest line 13
2. abbrev OAI.HarmonicArtin.restLabel line 14
3. def OAI.HarmonicArtin.labelSplit line 16
4. lemma OAI.HarmonicArtin.labelSplit_apply line 20
5. lemma OAI.HarmonicArtin.label_eq_iff line 23
6. lemma OAI.HarmonicArtin.restLabel_eq_iff line 29
7. def OAI.HarmonicArtin.FusionEdge.usesFactor line 35
8. def OAI.HarmonicArtin.FusionEdge.removeFactor line 40
9. lemma OAI.HarmonicArtin.stringMultiplicity_eq_ite line 45
10. lemma OAI.HarmonicArtin.factorMultiplicity_split_other line 52
11. lemma OAI.HarmonicArtin.FusionEdge.multiplicity_split line 70
12. def OAI.HarmonicArtin.fusionVertexSplit line 90