OAI/Geometry/HeilbronnTriangle/MinorInvariant.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem355.UnitPivot.MinorsVanish.mul_left line 13
  2. theorem OAI.Problem355.UnitPivot.minorsVanish_transpose_iff line 28
  3. theorem OAI.Problem355.UnitPivot.MinorsVanish.mul_right line 34
  4. theorem OAI.Problem355.UnitPivot.minorsVanish_unit_mul_iff line 41
  5. theorem OAI.Problem355.UnitPivot.minorsVanish_mul_unit_iff line 50
  6. theorem OAI.Problem355.UnitPivot.minorsVanish_equivalent_iff line 59
  7. theorem OAI.Problem355.UnitPivot.minorsVanish_diagonal_three_iff line 67
  8. theorem OAI.Problem355.UnitPivot.minorsVanish_diagonal_prime_power_iff line 76
  9. theorem OAI.Problem355.UnitPivot.minorsVanish_map_of_diagonal_form_iff line 85
  10. theorem OAI.Problem355.UnitPivot.minorsVanish_reduce_prime_power_iff line 106
  11. theorem OAI.Problem355.UnitPivot.smaller_exponent_eq_of_diagonal_forms line 121