OAI/Combinatorics/Progressions/Linear/MatrixSupInverse.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.matrix_det_abs_le_row_bounds line 17
  2. theorem OAI.Erdos3.matrix_det_abs_le_uniform_bound line 36
  3. theorem OAI.Erdos3.matrix_adjugate_entry_abs_le line 42
  4. theorem OAI.Erdos3.matrix_inverse_entry_abs_le line 66
  5. def OAI.Erdos3.matrixSupCLM line 88
  6. theorem OAI.Erdos3.matrixSupCLM_apply line 92
  7. theorem OAI.Erdos3.matrixSupCLM_norm_le line 95
  8. theorem OAI.Erdos3.matrixSupCLM_mul line 114
  9. theorem OAI.Erdos3.matrixSupCLM_one line 121
  10. theorem OAI.Erdos3.matrixSupCLM_inverse_spec line 127
  11. theorem OAI.Erdos3.matrixSupCLM_inverse_norm_le line 138