OAI/Topology/ArtinGroups/Harmonic/LeftSector.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.GraphConnection.LeftSector line 10
2. abbrev OAI.HarmonicArtin.GraphConnection.RightSector line 13
3. def OAI.HarmonicArtin.GraphConnection.sectorEquiv line 16
4. lemma OAI.HarmonicArtin.GraphConnection.scalar_sector_inverse line 34
5. lemma OAI.HarmonicArtin.GraphConnection.marked_sector_inverse line 51
6. def OAI.HarmonicArtin.GraphConnection.sectorSwitch line 75
7. lemma OAI.HarmonicArtin.GraphConnection.sectorSwitch_apply line 82
8. def OAI.HarmonicArtin.GraphConnection.sectorUnswitch line 88
9. lemma OAI.HarmonicArtin.GraphConnection.sector_inverse line 95