OAI/Topology/ArtinGroups/Harmonic/LiftedDeckOrderHom.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.liftedDeckOrderHom line 13
2. instance OAI.HarmonicArtin.liftedWeightsMulAction line 15
3. instance OAI.HarmonicArtin.liftedWeightsContinuousAction line 33
4. lemma OAI.HarmonicArtin.liftedWeights_smul_apply line 36
5. lemma OAI.HarmonicArtin.liftedDeck_comparable line 40
6. lemma OAI.HarmonicArtin.liftedWeights_disjoint_star line 51
7. def OAI.HarmonicArtin.SalvettiDeckQuotient line 66
8. instance OAI.HarmonicArtin.(instance at line 68) line 68
9. def OAI.HarmonicArtin.salvettiDeckProjection line 71
10. theorem OAI.HarmonicArtin.salvettiDeckProjection_quotientCovering line 73
11. theorem OAI.HarmonicArtin.salvettiDeckProjection_covering line 80
12. theorem OAI.HarmonicArtin.liftedWeights_contractible line 83