OAI/Geometry/HeilbronnTriangle/DigitObstruction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem355.DigitEncoding.no_small_representative line 10
  2. theorem OAI.Problem355.DigitEncoding.partial_sum_bound line 29
  3. theorem OAI.Problem355.DigitEncoding.distinguished_digit_bound line 43
  4. theorem OAI.Problem355.DigitEncoding.digit_obstruction line 56
  5. theorem OAI.Problem355.DigitEncoding.small_residue_forces_zero line 74
  6. theorem OAI.Problem355.DigitEncoding.sum_modEq_prefix line 81
  7. theorem OAI.Problem355.DigitEncoding.polynomial_eval_modEq_prefix line 92
  8. theorem OAI.Problem355.DigitEncoding.polynomial_obstruction line 98
  9. theorem OAI.Problem355.DigitEncoding.coefficient_bound_normalized line 106
  10. theorem OAI.Problem355.DigitEncoding.determinant_modEq line 113
  11. theorem OAI.Problem355.DigitEncoding.determinant_obstruction line 123
  12. theorem OAI.Problem355.DigitEncoding.determinant_modEq_of_specialLinear line 135