OAI/Analysis/MutuallyUnbiased/Cubic/CubicGraph.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.cubicGraph line 11
2. theorem OAI.MUB6.cubic_graph_entry line 15
3. theorem OAI.MUB6.cubic_graph_degree line 28
4. theorem OAI.MUB6.cubic_rows_agree_two line 38
5. theorem OAI.MUB6.cubic_graph_agreement line 49
6. theorem OAI.MUB6.cubic_graph_orthogonal line 66
7. theorem OAI.MUB6.tao_noninitial line 80