OAI/Combinatorics/HadwigerCounterexample/FourPhaseBits.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Four Phase Bits

  1. abbrev OAI.HadwigerCounterexample.Quad line 12
  2. def OAI.HadwigerCounterexample.quench line 14
  3. def OAI.HadwigerCounterexample.quadDot line 18
  4. def OAI.HadwigerCounterexample.quadPhase line 19
  5. theorem OAI.HadwigerCounterexample.party_card line 21
  6. theorem OAI.HadwigerCounterexample.quad_card line 22
  7. theorem OAI.HadwigerCounterexample.quad_rate line 23
  8. theorem OAI.HadwigerCounterexample.quad_inv_zero line 26
  9. theorem OAI.HadwigerCounterexample.quad_inv line 51
  10. theorem OAI.HadwigerCounterexample.joint_phase line 60
  11. theorem OAI.HadwigerCounterexample.quad_invert line 67
  12. theorem OAI.HadwigerCounterexample.mix_pattern line 76
  13. def OAI.HadwigerCounterexample.repeated line 102

    Source documentation

    common even relation on four scores.

    def repeated (x : Quad) :=
…

    Mentions: OAI.HadwigerCounterexample.Quad

  14. def OAI.HadwigerCounterexample.repeatQ line 105
  15. def OAI.HadwigerCounterexample.evenP line 107
  16. def OAI.HadwigerCounterexample.evenQ line 108
  17. theorem OAI.HadwigerCounterexample.party_single line 110
  18. theorem OAI.HadwigerCounterexample.even_dot line 120
  19. theorem OAI.HadwigerCounterexample.even_sum line 133
  20. theorem OAI.HadwigerCounterexample.tiny_pattern line 156