OAI/Topology/ArtinGroups/Harmonic/FrameFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.artinParabolic_univ line 21
2. lemma OAI.HarmonicArtin.sourceSignedWord_surjective line 27
3. def OAI.HarmonicArtin.sourceFrameFamily line 33
4. lemma OAI.HarmonicArtin.sourceFrameFamily_word line 36
5. lemma OAI.HarmonicArtin.sourceFrameFamily_mul line 42
6. def OAI.HarmonicArtin.sourceMultiplicity line 46
7. lemma OAI.HarmonicArtin.sourceMultiplicity_nonneg line 49
8. lemma OAI.HarmonicArtin.sourceMultiplicity_word line 52
9. lemma OAI.HarmonicArtin.sourceFrameFamily_exterior line 58
10. lemma OAI.HarmonicArtin.sourceMultiplicity_exterior line 65
11. lemma OAI.HarmonicArtin.sourceMultiplicity_frame line 74