OAI/Combinatorics/Progressions/Estimates/LowerTriangularMinor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_nonzero_row_minor line 14
  2. theorem OAI.Erdos3.nonzero_row_minor_injective line 33
  3. theorem OAI.Erdos3.exists_minimal_row_minor line 50
  4. theorem OAI.Erdos3.row_minor_update_det line 63
  5. theorem OAI.Erdos3.minimal_row_minor_coordinate_zero line 85
  6. theorem OAI.Erdos3.det_eq_one_of_triangular_labels line 118
  7. theorem OAI.Erdos3.lower_unitriangular_preserves_minimal_minor line 127
  8. theorem OAI.Erdos3.exists_preserved_nonzero_row_minor line 174