OAI/Combinatorics/HadwigerCounterexample/GramCharacterExpansion.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Gram Character Expansion

  1. def OAI.HadwigerCounterexample.vectorPhase line 14
  2. theorem OAI.HadwigerCounterexample.vector_expand line 16
  3. abbrev OAI.HadwigerCounterexample.Rail line 35
  4. def OAI.HadwigerCounterexample.ledgerM line 38
  5. def OAI.HadwigerCounterexample.railsM line 40
  6. def OAI.HadwigerCounterexample.traced line 42
  7. def OAI.HadwigerCounterexample.withinRail line 45
  8. theorem OAI.HadwigerCounterexample.inLedger line 49
  9. theorem OAI.HadwigerCounterexample.within_recorded line 55
  10. theorem OAI.HadwigerCounterexample.rail_charge line 58
  11. theorem OAI.HadwigerCounterexample.rail_expand line 80
  12. theorem OAI.HadwigerCounterexample.ledger_zero line 88
  13. theorem OAI.HadwigerCounterexample.phased_match line 91
  14. def OAI.HadwigerCounterexample.crowded line 94
  15. def OAI.HadwigerCounterexample.directions line 96
  16. theorem OAI.HadwigerCounterexample.match_crowd line 100
  17. theorem OAI.HadwigerCounterexample.rail_count line 116