OAI/Combinatorics/HadwigerCounterexample/MatrixQuotients.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Matrix Quotients

  1. def OAI.HadwigerCounterexample.box line 14
  2. theorem OAI.HadwigerCounterexample.box_dim line 17
  3. theorem OAI.HadwigerCounterexample.liftM_transpose line 25
  4. theorem OAI.HadwigerCounterexample.box_mem line 29
  5. theorem OAI.HadwigerCounterexample.box_le line 58
  6. theorem OAI.HadwigerCounterexample.pack_mem_iff line 63
  7. theorem OAI.HadwigerCounterexample.outer_in_box line 68
  8. theorem OAI.HadwigerCounterexample.lift_mem_box line 74
  9. theorem OAI.HadwigerCounterexample.evmat_transpose line 84
  10. theorem OAI.HadwigerCounterexample.evmat_pull line 86
  11. theorem OAI.HadwigerCounterexample.evmat_ext line 90
  12. theorem OAI.HadwigerCounterexample.box_eval_iff line 95
  13. def OAI.HadwigerCounterexample.annih line 110
  14. theorem OAI.HadwigerCounterexample.annih_dim line 112
  15. theorem OAI.HadwigerCounterexample.dot_ext_zero line 118
  16. theorem OAI.HadwigerCounterexample.annih_mem line 122
  17. theorem OAI.HadwigerCounterexample.annih_annih line 133
  18. def OAI.HadwigerCounterexample.vanish line 146
  19. theorem OAI.HadwigerCounterexample.rank_vanish line 150

    Source documentation

    A tensor killed by the product of the two factor quotients has bounded rank.

    theorem rank_vanish {S : Space (Vec I)} {T : Space (Vec J)} {M : Mat I J}
    (h : vanish S T M) : M.rank≤dim S+dim T := by
…

    Mentions: OAI.HadwigerCounterexample.Space, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.vanish, OAI.HadwigerCounterexample.dim