OAI/Topology/ArtinGroups/Harmonic/ResidueHeightZeroVector.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.sourceResidueHeight_zero_vector line 15
2. lemma OAI.HarmonicArtin.sourceResidueAllowed_closed_trans line 27
3. lemma OAI.HarmonicArtin.sourceResidue_zero_lower_iff line 40
4. lemma OAI.HarmonicArtin.sourceResidue_zero_exterior line 51
5. theorem OAI.HarmonicArtin.sourceResidue_zero_ne_lower line 74