OAI/Topology/ArtinGroups/Harmonic/FusionOrbitModel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.fusionOrbitModel line 22
2. lemma OAI.HarmonicArtin.fusionOrbitModel_minimal line 25
3. abbrev OAI.HarmonicArtin.FusionOrbitLayerIndex line 29
4. def OAI.HarmonicArtin.fusionOrbitLayer line 33
5. lemma OAI.HarmonicArtin.fusionOrbitLayer_middle line 38
6. lemma OAI.HarmonicArtin.fusionOrbitModel_negative_homDimension line 53
7. lemma OAI.HarmonicArtin.fusionOrbit_secondary_injective line 66
8. lemma OAI.HarmonicArtin.fusionOrbitLayer_cartan line 78