OAI/Combinatorics/HadwigerCounterexample/FreeBlockLinearAction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Free Block Linear Action

  1. abbrev OAI.HadwigerCounterexample.Flit line 12
  2. def OAI.HadwigerCounterexample.breeze line 14
  3. def OAI.HadwigerCounterexample.blitzL line 20
  4. def OAI.HadwigerCounterexample.blitz line 42
  5. theorem OAI.HadwigerCounterexample.blitz_val line 44
  6. theorem OAI.HadwigerCounterexample.blitz_mul line 49
  7. theorem OAI.HadwigerCounterexample.blitz_one line 61
  8. theorem OAI.HadwigerCounterexample.blitz_pick line 68
  9. theorem OAI.HadwigerCounterexample.blitz_fixes line 82
  10. def OAI.HadwigerCounterexample.doZ line 110

    Source documentation

    knobs player.

    def doZ (p : Shape) (M : Mat (Fin n) (Fin n)) (x : Knobs p.g n) :=
…

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.Knobs

  11. theorem OAI.HadwigerCounterexample.sailsZ line 113