OAI/Topology/ArtinGroups/ParabolicIntersections/PointedResidueHeightZero.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueHeight_zero_vector line 23
2. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidueAllowed_closed_trans line 35
3. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidue_zero_lower_iff line 48
4. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidue_zero_exterior line 59
5. theorem OAI.HarmonicArtin.ParabolicIntersections.pointedResidue_zero_ne_lower line 82