OAI/Topology/ArtinGroups/Realizations/LiftedWeightStar.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.liftedDeck_incident_finite line 13
2. def OAI.HarmonicArtin.liftedWeightStar line 27
3. lemma OAI.HarmonicArtin.liftedWeightStar_open line 31
4. lemma OAI.HarmonicArtin.liftedWeightStar_finite_translates line 35
5. instance OAI.HarmonicArtin.sourceDeckT2 line 45
6. instance OAI.HarmonicArtin.sourceSalvettiT2 line 80
7. instance OAI.HarmonicArtin.sourceModelCompact line 83
8. instance OAI.HarmonicArtin.sourceSalvettiCompact line 86