OAI/Geometry/HeilbronnTriangle/PivotAssembly.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem355.PivotAssembly.exists_unit_pivot_reduction line 12
  2. def OAI.Problem355.PivotAssembly.embedTwo line 39
  3. theorem OAI.Problem355.PivotAssembly.embedTwo_mul line 42
  4. theorem OAI.Problem355.PivotAssembly.det_embedTwo line 48
  5. theorem OAI.Problem355.PivotAssembly.embedTwo_diagonal line 52
  6. theorem OAI.Problem355.PivotAssembly.exists_diagonal_of_two_by_two line 57
  7. theorem OAI.Problem355.PivotAssembly.factorization_of_reduction line 81
  8. theorem OAI.Problem355.PivotAssembly.exists_factorization_of_two_by_two line 94
  9. theorem OAI.Problem355.PivotAssembly.exists_factorization_of_two_by_two_units line 108