OAI/Topology/ArtinGroups/Harmonic/CosetVectorNullPatch.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.sourceCosetVector_of_null_patch line 17
2. theorem OAI.HarmonicArtin.sourceClosedResidue_nonempty line 36
3. lemma OAI.HarmonicArtin.sourceResidue_empty_type line 93