OAI/Topology/ArtinGroups/Harmonic/ResidueAllowed.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.SourceResidueAllowed line 12
2. abbrev OAI.HarmonicArtin.SourceResidue line 18
3. def OAI.HarmonicArtin.sourceResidueHeight line 21
4. lemma OAI.HarmonicArtin.sourceCosetVector_lower_compare_int line 24
5. lemma OAI.HarmonicArtin.sourceCosetVector_lower_compare_int_rev line 38
6. lemma OAI.HarmonicArtin.sourceResidueAllowed_le line 52
7. lemma OAI.HarmonicArtin.sourceResidueHeight_nonpos line 61
8. lemma OAI.HarmonicArtin.sourceResidueHeight_strict line 65
9. lemma OAI.HarmonicArtin.sourceResidueHeight_mono line 72
10. lemma OAI.HarmonicArtin.sourceResidueHeight_lt line 77
11. lemma OAI.HarmonicArtin.sourceResidueAllowed_upper line 85