OAI/Topology/ArtinGroups/Harmonic/UnfoldedInclusion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.unfoldedInclusion line 16
2. lemma OAI.HarmonicArtin.unfoldedInclusion_injective line 21
3. lemma OAI.HarmonicArtin.unfolded_ordinaryMatrix line 29
4. lemma OAI.HarmonicArtin.unfolded_full_simply_laced line 51
5. lemma OAI.HarmonicArtin.fusionExpandedWord_map line 67
6. theorem OAI.HarmonicArtin.unfolded_full_reduced line 76
7. lemma OAI.HarmonicArtin.fusionExpandedWord_mem line 84