OAI/Combinatorics/Crossing/PlanarDeterminant.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Zarankiewicz.det2_add_left line 7
  2. theorem OAI.Zarankiewicz.det2_add_right line 11
  3. theorem OAI.Zarankiewicz.det2_sub_left line 15
  4. theorem OAI.Zarankiewicz.det2_sub_right line 19
  5. theorem OAI.Zarankiewicz.det2_smul_left line 23
  6. theorem OAI.Zarankiewicz.det2_smul_right line 27
  7. theorem OAI.Zarankiewicz.det2_self line 31
  8. theorem OAI.Zarankiewicz.det2_zero_left line 35
  9. theorem OAI.Zarankiewicz.det2_zero_right line 36