OAI/Topology/ArtinGroups/Harmonic/Eligible.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.SourceEligible line 12
2. lemma OAI.HarmonicArtin.sourceCosetVector_open line 19
3. lemma OAI.HarmonicArtin.source_ineligible_top_ge line 25
4. lemma OAI.HarmonicArtin.source_eligible_top_le line 43
5. lemma OAI.HarmonicArtin.sourceCosetSign_eq_at_lower_tie line 57
6. lemma OAI.HarmonicArtin.sourceLowerLevel_prescribed_at_tie line 67
7. lemma OAI.HarmonicArtin.source_ineligible_tie_sign line 78
8. lemma OAI.HarmonicArtin.source_eligible_tie_sign line 100