OAI/Geometry/HeilbronnTriangle/MainDigitLaw.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem355.MainDigitLaw.Sample line 20
  2. abbrev OAI.Problem355.MainDigitLaw.Latent line 21
  3. abbrev OAI.Problem355.MainDigitLaw.Array line 23
  4. lemma OAI.Problem355.MainDigitLaw.alphabet_bound line 28
  5. def OAI.Problem355.MainDigitLaw.digit line 32
  6. lemma OAI.Problem355.MainDigitLaw.digit_injective line 37
  7. lemma OAI.Problem355.MainDigitLaw.digit_positive line 42
  8. lemma OAI.Problem355.MainDigitLaw.digit_le line 47
  9. lemma OAI.Problem355.MainDigitLaw.digit_residue line 55
  10. def OAI.Problem355.MainDigitLaw.column line 62
  11. def OAI.Problem355.MainDigitLaw.arrayDigit line 65
  12. def OAI.Problem355.MainDigitLaw.matrix line 69
  13. lemma OAI.Problem355.MainDigitLaw.column_matrix line 74
  14. def OAI.Problem355.MainDigitLaw.smith line 78
  15. lemma OAI.Problem355.MainDigitLaw.moment_parameter line 85
  16. theorem OAI.Problem355.MainDigitLaw.conditional_moment line 92
  17. theorem OAI.Problem355.MainDigitLaw.triple_moment line 102