OAI/Topology/ArtinGroups/Harmonic/IncidentNonnegRowPositive.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.source_incident_nonneg_row_positive line 13
2. lemma OAI.HarmonicArtin.sourceActive_iff line 32
3. lemma OAI.HarmonicArtin.sourceCosetSign_eq_one_of_not_negative line 47
4. lemma OAI.HarmonicArtin.source_inactive_top_rows line 57
5. lemma OAI.HarmonicArtin.source_active_top_rows line 70
6. lemma OAI.HarmonicArtin.source_inactive_sign line 82
7. lemma OAI.HarmonicArtin.source_active_sign line 92