OAI/Topology/ArtinGroups/Harmonic/ResidueEarlierLowerIso.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.sourceResidueEarlier_total line 18
2. def OAI.HarmonicArtin.sourceResidueEarlierLowerIso line 23
3. def OAI.HarmonicArtin.sourceResidueEarlierUpperIso line 36
4. lemma OAI.HarmonicArtin.sourceResidue_lower_boundary line 48
5. lemma OAI.HarmonicArtin.sourceResidue_upper_weights_contractible line 62
6. lemma OAI.HarmonicArtin.sourceResidue_emptyLink_upper line 72
7. lemma OAI.HarmonicArtin.sourceResidue_emptyLink_lower line 80