OAI/Topology/ArtinGroups/ParabolicIntersections/PointedResidueAllowed.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ParabolicIntersections.PointedResidueAllowed line 17
2. abbrev OAI.HarmonicArtin.ParabolicIntersections.PointedResidue line 23
3. def OAI.HarmonicArtin.ParabolicIntersections.pointedResidueHeight line 26
4. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_lower_compare_int line 29
5. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_lower_compare_int_rev line 43
6. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueAllowed_le line 57
7. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueHeight_nonpos line 66
8. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueHeight_strict line 70
9. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueHeight_mono line 77
10. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueHeight_lt line 82
11. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueAllowed_upper line 90