OAI/LinearAlgebra/MatrixFields/CapacityA/CapA5_5_6I0.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0Value line 16
  2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0Raw line 17
  3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0Raw_sound line 18
  4. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0Certificates line 21
  5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0Certificates_valid line 26
  6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0CertificateIndex line 28
  7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0P line 37
  8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0P_check line 39
  9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0P_sound line 41
  10. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0Terms line 44
  11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0Terms_sound line 46
  12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0Entropy line 50
  13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0Entropy_sound line 51
  14. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0Mass line 53
  15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0Mass_sound line 54
  16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0MassTermLogWitness line 56
  17. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0MassTermLog line 57
  18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0MassTermLog_sound line 58
  19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0MassTerm line 62
  20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0MassTerm_sound line 63
  21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0H line 65
  22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0H_sound line 66
  23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA5_5_6I0_sound line 68