OAI/LinearAlgebra/MatrixFields/Certificates/Four0_1_7.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7Value line 15
  2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7E_4_5LogWitness line 16
  3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7E_4_5Log line 17
  4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7E_4_5Log_sound line 18
  5. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7E_4_5 line 22
  6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7E_4_5_sound line 23
  7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7E_5_4LogWitness line 25
  8. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7E_5_4Log line 26
  9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7E_5_4Log_sound line 27
  10. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7E_5_4 line 31
  11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7E_5_4_sound line 32
  12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7Terms line 34
  13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7Terms_sound line 39
  14. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7Entropy line 50
  15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7Entropy_sound line 51
  16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7Labels line 53
  17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7Labels_sound line 54
  18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7Four line 59
  19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7Four_sound line 60
  20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0Value line 62
  21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0E_0_0Log line 63
  22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0E_0_0Log_sound line 64
  23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0E_0_0 line 66
  24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0E_0_0_sound line 67
  25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0Terms line 69
  26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0Terms_sound line 73
  27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0Entropy line 84
  28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0Entropy_sound line 85
  29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0Mass line 87
  30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0Mass_sound line 88
  31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0MassTermLog line 90
  32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0MassTermLog_sound line 91
  33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0MassTerm line 93
  34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0MassTerm_sound line 94
  35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0H line 96
  36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H0H_sound line 97
  37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1Value line 99
  38. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1E_1_0LogWitness line 100
  39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1E_1_0Log line 101
  40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1E_1_0Log_sound line 102
  41. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1E_1_0 line 106
  42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1E_1_0_sound line 107
  43. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1E_0_1LogWitness line 109
  44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1E_0_1Log line 110
  45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1E_0_1Log_sound line 111
  46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1E_0_1 line 115
  47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1E_0_1_sound line 116
  48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1Terms line 118
  49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1Terms_sound line 123
  50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1Entropy line 134
  51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1Entropy_sound line 135
  52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1Mass line 137
  53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1Mass_sound line 138
  54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1MassTermLog line 140
  55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1MassTermLog_sound line 141
  56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1MassTerm line 143
  57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1MassTerm_sound line 144
  58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1H line 146
  59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H1H_sound line 147
  60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2Value line 149
  61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2E_4_5LogWitness line 150
  62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2E_4_5Log line 151
  63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2E_4_5Log_sound line 152
  64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2E_4_5 line 156
  65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2E_4_5_sound line 157
  66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2E_5_4LogWitness line 159
  67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2E_5_4Log line 160
  68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2E_5_4Log_sound line 161
  69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2E_5_4 line 165
  70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2E_5_4_sound line 166
  71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2Terms line 168
  72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2Terms_sound line 173
  73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2Entropy line 184
  74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2Entropy_sound line 185
  75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2Mass line 187
  76. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2Mass_sound line 188
  77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2MassTermLog line 190
  78. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2MassTermLog_sound line 191
  79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2MassTerm line 193
  80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2MassTerm_sound line 194
  81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2H line 196
  82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_1_7H2H_sound line 197