OAI/Combinatorics/HadwigerCounterexample/MatrixRankCounting.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Matrix Rank Counting

  1. theorem OAI.HadwigerCounterexample.cast_mat line 13
  2. theorem OAI.HadwigerCounterexample.nbr_nonneg line 19
  3. theorem OAI.HadwigerCounterexample.nbr_le_sum line 22
  4. theorem OAI.HadwigerCounterexample.mul_factor line 34
  5. theorem OAI.HadwigerCounterexample.nbr_matrix_rank line 42
  6. theorem OAI.HadwigerCounterexample.pr_matrix_rank line 65
  7. def OAI.HadwigerCounterexample.rmult line 71
  8. theorem OAI.HadwigerCounterexample.pr_mult_mat line 76
  9. theorem OAI.HadwigerCounterexample.pr_deficient line 84
  10. def OAI.HadwigerCounterexample.profileA line 121
  11. theorem OAI.HadwigerCounterexample.nbr_profile_rank line 123
  12. theorem OAI.HadwigerCounterexample.profile_count line 159