OAI/Topology/ArtinGroups/Realizations/WeightDim.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.HarmonicArtin.orderWeightSupportLinearOrder line 14
2. def OAI.HarmonicArtin.weightDim line 20
3. lemma OAI.HarmonicArtin.weightDim_succ line 22
4. def OAI.HarmonicArtin.weightEnum line 27
5. def OAI.HarmonicArtin.weightChain line 31
6. lemma OAI.HarmonicArtin.weightChain_injective line 35
7. def OAI.HarmonicArtin.weightSimplex line 38
8. lemma OAI.HarmonicArtin.chainWeights_injective_apply line 48
9. lemma OAI.HarmonicArtin.orderWeightsOfChain_canonical line 57
10. lemma OAI.HarmonicArtin.chainWeights_coordinates_injective line 75