OAI/Topology/ArtinGroups/Harmonic/ResidueRank.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.sourceResidueHeight_range_finite line 12
2. def OAI.HarmonicArtin.sourceResidueRank line 21
3. lemma OAI.HarmonicArtin.sourceResidueRank_strictMono line 24
4. lemma OAI.HarmonicArtin.sourceResidueRank_lt_iff line 32
5. lemma OAI.HarmonicArtin.sourceResidueRank_eq_iff line 47
6. def OAI.HarmonicArtin.sourceResidueSecondary line 60
7. def OAI.HarmonicArtin.sourceResidueKey line 63
8. def OAI.HarmonicArtin.SourceResidueEarlier line 68
9. lemma OAI.HarmonicArtin.sourceResidueKey_injective line 71
10. theorem OAI.HarmonicArtin.sourceResidueEarlier_wellFounded line 78
11. lemma OAI.HarmonicArtin.sourceResidueEarlier_iff line 82
12. lemma OAI.HarmonicArtin.sourceResidueEarlier_lower_negative line 93
13. lemma OAI.HarmonicArtin.sourceResidueEarlier_upper_negative line 107
14. lemma OAI.HarmonicArtin.sourceResidueEarlier_lower_zero line 125
15. lemma OAI.HarmonicArtin.sourceResidueEarlier_upper_zero line 135