OAI/Topology/ArtinGroups/Harmonic/FusionOrbitMultiplicity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.finite_weighted_cartan line 16
2. def OAI.HarmonicArtin.fusionOrbitMultiplicity line 35
3. lemma OAI.HarmonicArtin.fusionOrbitMultiplicity_nonneg line 38
4. def OAI.HarmonicArtin.fusionOrbitWeightedVector line 42
5. lemma OAI.HarmonicArtin.fusionOrbitLayer_generator line 45
6. lemma OAI.HarmonicArtin.fusionOrbitWeightedVector_eq line 50
7. def OAI.HarmonicArtin.fusionOrbitLayerHom line 59
8. lemma OAI.HarmonicArtin.fusionOrbitLayerHom_nonneg line 63
9. theorem OAI.HarmonicArtin.fusionOrbit_weighted_euler line 71
10. lemma OAI.HarmonicArtin.fusionOrbit_cartan_nonneg line 95