OAI/Combinatorics/HadwigerCounterexample/PrimalSpaceCompression.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Primal Space Compression

  1. theorem OAI.HadwigerCounterexample.exists_cover line 13
  2. theorem OAI.HadwigerCounterexample.compact_endo line 30
  3. abbrev OAI.HadwigerCounterexample.Sel line 44
  4. abbrev OAI.HadwigerCounterexample.Nendo line 45
  5. def OAI.HadwigerCounterexample.iFix line 46
  6. def OAI.HadwigerCounterexample.iCoeff line 47
  7. def OAI.HadwigerCounterexample.rowShrink line 51

    Source documentation

    induced row vector transform.

    def rowShrink (p : Shape) {n} (A : Nendo p n) : Mat (Row p n) (Row p n) :=
…

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Nendo, OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.Row

  8. def OAI.HadwigerCounterexample.readCoeff line 55
  9. theorem OAI.HadwigerCounterexample.readCoeff_val line 58
  10. theorem OAI.HadwigerCounterexample.shrink_transpose line 61
  11. theorem OAI.HadwigerCounterexample.coeff_none line 66
  12. theorem OAI.HadwigerCounterexample.coeff_some line 75
  13. theorem OAI.HadwigerCounterexample.coeff_fixes line 94
  14. def OAI.HadwigerCounterexample.nbBlock line 103
  15. def OAI.HadwigerCounterexample.ncComp line 104
  16. theorem OAI.HadwigerCounterexample.shrink_rank line 106
  17. def OAI.HadwigerCounterexample.dbits line 117
  18. def OAI.HadwigerCounterexample.drow line 118
  19. theorem OAI.HadwigerCounterexample.shrink_both line 120
  20. def OAI.HadwigerCounterexample.shrinkBase line 157
  21. theorem OAI.HadwigerCounterexample.shrink_point line 160
  22. theorem OAI.HadwigerCounterexample.shrink_tag line 171
  23. theorem OAI.HadwigerCounterexample.shrink_X line 188