OAI/Topology/ArtinGroups/Harmonic/PositiveWord.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.sourcePositiveWord line 22
2. def OAI.HarmonicArtin.sourceBottomWord line 26
3. lemma OAI.HarmonicArtin.sourcePositiveWord_cons line 30
4. lemma OAI.HarmonicArtin.sourcePositiveWord_lowerBound line 35
5. lemma OAI.HarmonicArtin.sourcePositiveWord_reduced_eq line 42
6. lemma OAI.HarmonicArtin.sourceBottomWord_cons_socle_zero line 59
7. theorem OAI.HarmonicArtin.sourceBottomWord_socle_ascent line 68
8. lemma OAI.HarmonicArtin.bounded_word_saturation line 91
9. theorem OAI.HarmonicArtin.source_socle_finite_termination line 114