OAI/Topology/ArtinGroups/Harmonic/ResidueZeroLowerIso.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.HarmonicArtin.sourceResidue_lower_weights_contractibleline 16 - def
OAI.HarmonicArtin.sourceResidueZeroLowerIsoline 31 - lemma
OAI.HarmonicArtin.sourceResidueZeroUpper_emptyline 41 - lemma
OAI.HarmonicArtin.sourceResidue_special_boundaryline 47