OAI/Geometry/HeilbronnTriangle/PrimitiveNormal.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem355.PrimitiveNormal.Vector line 11
  2. def OAI.Problem355.PrimitiveNormal.coordGcd line 13
  3. def OAI.Problem355.PrimitiveNormal.IsPrimitive line 16
  4. lemma OAI.Problem355.PrimitiveNormal.coordGcd_eq_zero_iff line 18
  5. lemma OAI.Problem355.PrimitiveNormal.coordGcd_dvd line 30
  6. lemma OAI.Problem355.PrimitiveNormal.exists_dot_eq_coordGcd line 38
  7. lemma OAI.Problem355.PrimitiveNormal.isPrimitive_iff_exists_dot_eq_one line 53
  8. lemma OAI.Problem355.PrimitiveNormal.IsPrimitive.ne_zero line 70
  9. theorem OAI.Problem355.PrimitiveNormal.exists_primitive_factor line 76
  10. lemma OAI.Problem355.PrimitiveNormal.coordinate_abs_le_of_factor line 97
  11. theorem OAI.Problem355.PrimitiveNormal.exists_primitive_normal line 103
  12. def OAI.Problem355.PrimitiveNormal.rowNormals line 118
  13. lemma OAI.Problem355.PrimitiveNormal.mulVec_rowNormals line 121
  14. lemma OAI.Problem355.PrimitiveNormal.exists_rowNormal_ne_zero line 126
  15. lemma OAI.Problem355.PrimitiveNormal.coefficients_zero_of_cross_ne_zero line 138
  16. lemma OAI.Problem355.PrimitiveNormal.kernel_coordinates_ne_zero line 154
  17. lemma OAI.Problem355.PrimitiveNormal.abs_minor_le line 187
  18. lemma OAI.Problem355.PrimitiveNormal.cross_coordinate_bound line 198
  19. theorem OAI.Problem355.PrimitiveNormal.exists_primitive_right_null line 204
  20. theorem OAI.Problem355.PrimitiveNormal.primitive_eq_or_eq_neg_of_cross_eq_zero line 224
  21. lemma OAI.Problem355.PrimitiveNormal.cross_ne_zero_of_projective_ne line 247
  22. theorem OAI.Problem355.PrimitiveNormal.exists_primitive_right_null_of_projections line 267
  23. def OAI.Problem355.PrimitiveNormal.toEuclidean line 279
  24. lemma OAI.Problem355.PrimitiveNormal.norm_le_three_mul_of_coordinate_bound line 282
  25. theorem OAI.Problem355.PrimitiveNormal.exists_bounded_primitive_right_null line 294
  26. lemma OAI.Problem355.PrimitiveNormal.one_le_norm_of_ne_zero line 309
  27. lemma OAI.Problem355.PrimitiveNormal.modulus_le_norm_of_coordinate_zero line 319
  28. theorem OAI.Problem355.PrimitiveNormal.modulus_le_norm_of_reduction_in_difference_line line 330
  29. lemma OAI.Problem355.PrimitiveNormal.half_modulus_lt_shell_radius line 342