OAI/Topology/ArtinGroups/Harmonic/RestrictedArtinHom.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.restrictedArtin_relators line 13
2. def OAI.HarmonicArtin.restrictedArtinHom line 27
3. lemma OAI.HarmonicArtin.restrictedArtinHom_generator line 30
4. lemma OAI.HarmonicArtin.restrictedArtinHom_word line 34
5. lemma OAI.HarmonicArtin.restrictedArtinHom_range line 43
6. theorem OAI.HarmonicArtin.sphericalParabolic_positive_fraction line 62