OAI/Topology/ArtinGroups/Harmonic/PositiveSimpleLiftMul.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.positiveSimpleLift_mul line 15
2. lemma OAI.HarmonicArtin.positive_simple_factors line 32
3. lemma OAI.HarmonicArtin.longest_inverse_eq line 47
4. lemma OAI.HarmonicArtin.length_mul_longest line 52
5. lemma OAI.HarmonicArtin.positiveSimpleLift_left_complement line 59
6. lemma OAI.HarmonicArtin.positiveSimpleLift_right_complement line 66
7. theorem OAI.HarmonicArtin.positive_fundamental_left_divisor_iff line 73
8. theorem OAI.HarmonicArtin.positive_fundamental_right_divisor_iff line 82