OAI/Analysis/MutuallyUnbiased/Cubic/FiveCycle.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A finite, kernel-checked classification of simple two-regular graphs on five vertices. Ten Boolean edge choices are checked, not matrices over a restricted alphabet.

  1. def OAI.MUB6.fiveGraph line 13
  2. def OAI.MUB6.twoRegularFive line 20
  3. def OAI.MUB6.fiveCycleOrder line 23
  4. def OAI.MUB6.canonicalFiveCycle line 28
  5. theorem OAI.MUB6.fiveCycleOrder_bijective line 31
  6. theorem OAI.MUB6.twoRegularFive_is_cycle line 34
  7. def OAI.MUB6.fiveCyclePermutation line 40