OAI/Topology/ArtinGroups/Harmonic/RootExtension.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.rootExtension line 13
2. lemma OAI.HarmonicArtin.rootExtension_apply line 16
3. lemma OAI.HarmonicArtin.rootExtension_outside line 23
4. lemma OAI.HarmonicArtin.rootExtension_restrict line 32
5. lemma OAI.HarmonicArtin.rootExtension_sub line 41
6. lemma OAI.HarmonicArtin.rootExtension_smul line 46
7. lemma OAI.HarmonicArtin.rootExtension_single line 51
8. lemma OAI.HarmonicArtin.rootExtension_mulVec line 56
9. lemma OAI.HarmonicArtin.rowReflect_rootExtension line 65
10. lemma OAI.HarmonicArtin.rowReflectWord_rootExtension line 69
11. lemma OAI.HarmonicArtin.rowReflectWord_harmonic line 79
12. def OAI.HarmonicArtin.sourceRootInclusion line 90
13. lemma OAI.HarmonicArtin.sourceRootInclusion_injective line 93
14. lemma OAI.HarmonicArtin.source_folded_submatrix line 97
15. lemma OAI.HarmonicArtin.sourceRoot_word_representation line 110