OAI/Topology/ArtinGroups/Harmonic/Coset.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.sourceCoset line 12
2. lemma OAI.HarmonicArtin.rightCoset_mono line 16
3. lemma OAI.HarmonicArtin.rightCoset_eq_of_mem line 20
4. lemma OAI.HarmonicArtin.sourceCoset_le line 26
5. lemma OAI.HarmonicArtin.sourceCosetRepresentative_mem line 31
6. lemma OAI.HarmonicArtin.sourceCoset_eq line 36
7. lemma OAI.HarmonicArtin.deligne_eq_of_le_type_eq line 46
8. lemma OAI.HarmonicArtin.deligne_lt_type line 56
9. lemma OAI.HarmonicArtin.sourceCosetVector_harmonic line 59
10. lemma OAI.HarmonicArtin.sourceCosetVector_upper_outside line 64
11. lemma OAI.HarmonicArtin.sourceCosetVector_upper_harmonize line 73
12. theorem OAI.HarmonicArtin.sourceCosetVector_upper_change line 79