OAI/Analysis/Quantum/PPTSquare/Mod139Reduction.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ModularPencil.P139.matrix_reduce_row0 line 12
  2. lemma OAI.ModularPencil.P139.matrix_reduce_row1 line 13
  3. lemma OAI.ModularPencil.P139.matrix_reduce_row2 line 14
  4. lemma OAI.ModularPencil.P139.matrix_reduce_row3 line 15
  5. lemma OAI.ModularPencil.P139.matrix_reduce_row4 line 16
  6. lemma OAI.ModularPencil.P139.matrix_reduce_row5 line 17
  7. lemma OAI.ModularPencil.P139.matrix_reduce_row6 line 18
  8. lemma OAI.ModularPencil.P139.matrix_reduce_row7 line 19
  9. lemma OAI.ModularPencil.P139.matrix_reduce_row8 line 20
  10. lemma OAI.ModularPencil.P139.matrix_reduce_row9 line 21
  11. lemma OAI.ModularPencil.P139.matrix_reduce_row10 line 22
  12. lemma OAI.ModularPencil.P139.matrix_reduce_row11 line 23
  13. lemma OAI.ModularPencil.P139.matrix_reduce_row12 line 24
  14. lemma OAI.ModularPencil.P139.matrix_reduce_row13 line 25
  15. lemma OAI.ModularPencil.P139.matrix_reduce_row14 line 26
  16. lemma OAI.ModularPencil.P139.matrix_reduce_row15 line 27
  17. lemma OAI.ModularPencil.P139.matrix_reduce_row16 line 28
  18. lemma OAI.ModularPencil.P139.matrix_reduce_row17 line 29
  19. lemma OAI.ModularPencil.P139.matrix_reduce_row18 line 30
  20. lemma OAI.ModularPencil.P139.matrix_reduce_row19 line 31
  21. lemma OAI.ModularPencil.P139.matrix_reduce line 32
  22. lemma OAI.ModularPencil.P139.first_column line 55
  23. lemma OAI.ModularPencil.P139.UV_row0 line 56
  24. lemma OAI.ModularPencil.P139.UV_row1 line 57
  25. lemma OAI.ModularPencil.P139.UV_row2 line 58
  26. lemma OAI.ModularPencil.P139.UV_row3 line 59
  27. lemma OAI.ModularPencil.P139.UV_row4 line 60
  28. lemma OAI.ModularPencil.P139.UV_row5 line 61
  29. lemma OAI.ModularPencil.P139.UV_row6 line 62
  30. lemma OAI.ModularPencil.P139.UV_row7 line 63
  31. lemma OAI.ModularPencil.P139.UV_row8 line 64
  32. lemma OAI.ModularPencil.P139.UV_row9 line 65
  33. lemma OAI.ModularPencil.P139.UV_row10 line 66
  34. lemma OAI.ModularPencil.P139.UV_row11 line 67
  35. lemma OAI.ModularPencil.P139.UV_row12 line 68
  36. lemma OAI.ModularPencil.P139.UV_row13 line 69
  37. lemma OAI.ModularPencil.P139.UV_row14 line 70
  38. lemma OAI.ModularPencil.P139.UV_row15 line 71
  39. lemma OAI.ModularPencil.P139.UV_row16 line 72
  40. lemma OAI.ModularPencil.P139.UV_row17 line 73
  41. lemma OAI.ModularPencil.P139.UV_row18 line 74
  42. lemma OAI.ModularPencil.P139.UV_row19 line 75
  43. lemma OAI.ModularPencil.P139.UV line 76