OAI/Geometry/HeilbronnTriangle/ConditionalMatrix.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem355.ConditionalMatrix.Header line 12
  2. abbrev OAI.Problem355.ConditionalMatrix.Draw line 15
  3. def OAI.Problem355.ConditionalMatrix.picked line 18
  4. def OAI.Problem355.ConditionalMatrix.drawEquiv line 22
  5. def OAI.Problem355.ConditionalMatrix.entryValue line 37
  6. def OAI.Problem355.ConditionalMatrix.residueMatrix line 42
  7. def OAI.Problem355.ConditionalMatrix.arrayMatrix line 47
  8. lemma OAI.Problem355.ConditionalMatrix.residueMatrix_eq_arrayMatrix line 53
  9. theorem OAI.Problem355.ConditionalMatrix.encoded_isUnit line 57
  10. theorem OAI.Problem355.ConditionalMatrix.moment_le_two line 71
  11. theorem OAI.Problem355.ConditionalMatrix.array_moment_le_two line 107
  12. def OAI.Problem355.ConditionalMatrix.prescribedDigit line 128
  13. lemma OAI.Problem355.ConditionalMatrix.prescribedDigit_injective line 134
  14. lemma OAI.Problem355.ConditionalMatrix.prescribedDigit_positive line 142
  15. lemma OAI.Problem355.ConditionalMatrix.prescribedDigit_residue line 147
  16. theorem OAI.Problem355.ConditionalMatrix.prescribed_moment_le_two line 152