OAI/Topology/ArtinGroups/Harmonic/PositivePrefix.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.PositivePrefix line 13
2. lemma OAI.HarmonicArtin.positivePrefix_refl line 15
3. lemma OAI.HarmonicArtin.positivePrefix_one line 16
4. lemma OAI.HarmonicArtin.positivePrefix_trans line 17
5. lemma OAI.HarmonicArtin.positivePrefix_degree line 21
6. lemma OAI.HarmonicArtin.positivePrefix_eq_of_degree line 25
7. lemma OAI.HarmonicArtin.positivePrefix_antisymm line 32
8. lemma OAI.HarmonicArtin.positivePrefix_simple_iff line 37
9. lemma OAI.HarmonicArtin.positivePrefix_of_simple_eq line 54
10. theorem OAI.HarmonicArtin.exists_greatest_common_simplePrefix line 60
11. lemma OAI.HarmonicArtin.positiveSimpleLift_simple line 73
12. lemma OAI.HarmonicArtin.positiveSimpleLift_one line 79