OAI/Topology/ArtinGroups/Harmonic/FusionPacketPerm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.fusionColor_orthogonal line 23
2. def OAI.HarmonicArtin.fusionPacketPerm line 27
3. def OAI.HarmonicArtin.fusionSignedPacketPerm line 30
4. def OAI.HarmonicArtin.fusionWordPacketPerm line 35
5. lemma OAI.HarmonicArtin.restFusion_symmetric line 46
6. lemma OAI.HarmonicArtin.restFusion_diagonal line 51
7. lemma OAI.HarmonicArtin.fusionPacket_split line 67
8. lemma OAI.HarmonicArtin.fusionSignedPacket_split line 103
9. lemma OAI.HarmonicArtin.fusionWord_split line 121