OAI/Topology/ArtinGroups/Harmonic/SwitchIndex.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.GraphConnection.SwitchIndex line 11
2. def OAI.HarmonicArtin.GraphConnection.switchMatrix line 13
3. def OAI.HarmonicArtin.GraphConnection.unswitchMatrix line 17
4. lemma OAI.HarmonicArtin.GraphConnection.switch_unswitch line 21
5. lemma OAI.HarmonicArtin.GraphConnection.unswitch_switch line 44
6. def OAI.HarmonicArtin.GraphConnection.switchEquiv line 50