OAI/Analysis/Quantum/PPTSquare/Multiplication.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PencilAlgebra.NNum line 9
  2. def OAI.PencilAlgebra.lowNext line 10
  3. def OAI.PencilAlgebra.highNext line 11
  4. lemma OAI.PencilAlgebra.low_col_0_0 line 12
  5. lemma OAI.PencilAlgebra.low_col_0_1 line 13
  6. lemma OAI.PencilAlgebra.low_col_0_2 line 14
  7. lemma OAI.PencilAlgebra.low_col_0_3 line 15
  8. lemma OAI.PencilAlgebra.low_col_0_4 line 16
  9. lemma OAI.PencilAlgebra.low_col_0_5 line 17
  10. lemma OAI.PencilAlgebra.low_col_0_6 line 18
  11. lemma OAI.PencilAlgebra.low_col_0_7 line 19
  12. lemma OAI.PencilAlgebra.low_col_0_8 line 20
  13. lemma OAI.PencilAlgebra.low_col_0_9 line 21
  14. lemma OAI.PencilAlgebra.high_col_0_0 line 22
  15. lemma OAI.PencilAlgebra.high_col_0_1 line 23
  16. lemma OAI.PencilAlgebra.high_col_0_2 line 24
  17. lemma OAI.PencilAlgebra.high_col_0_3 line 25
  18. lemma OAI.PencilAlgebra.high_col_0_4 line 26
  19. lemma OAI.PencilAlgebra.high_col_0_5 line 27
  20. lemma OAI.PencilAlgebra.high_col_0_6 line 28
  21. lemma OAI.PencilAlgebra.high_col_0_7 line 29
  22. lemma OAI.PencilAlgebra.high_col_0_8 line 30
  23. lemma OAI.PencilAlgebra.high_col_0_9 line 31
  24. lemma OAI.PencilAlgebra.low_col_1_0 line 32
  25. lemma OAI.PencilAlgebra.low_col_1_1 line 33
  26. lemma OAI.PencilAlgebra.low_col_1_2 line 34
  27. lemma OAI.PencilAlgebra.low_col_1_3 line 35
  28. lemma OAI.PencilAlgebra.low_col_1_4 line 36
  29. lemma OAI.PencilAlgebra.low_col_1_5 line 37
  30. lemma OAI.PencilAlgebra.low_col_1_6 line 38
  31. lemma OAI.PencilAlgebra.low_col_1_7 line 39
  32. lemma OAI.PencilAlgebra.low_col_1_8 line 40
  33. lemma OAI.PencilAlgebra.low_col_1_9 line 41
  34. lemma OAI.PencilAlgebra.high_col_1_0 line 42
  35. lemma OAI.PencilAlgebra.high_col_1_1 line 43
  36. lemma OAI.PencilAlgebra.high_col_1_2 line 44
  37. lemma OAI.PencilAlgebra.high_col_1_3 line 45
  38. lemma OAI.PencilAlgebra.high_col_1_4 line 46
  39. lemma OAI.PencilAlgebra.high_col_1_5 line 47
  40. lemma OAI.PencilAlgebra.high_col_1_6 line 48
  41. lemma OAI.PencilAlgebra.high_col_1_7 line 49
  42. lemma OAI.PencilAlgebra.high_col_1_8 line 50
  43. lemma OAI.PencilAlgebra.high_col_1_9 line 51
  44. lemma OAI.PencilAlgebra.low_col_2_0 line 52
  45. lemma OAI.PencilAlgebra.low_col_2_1 line 53
  46. lemma OAI.PencilAlgebra.low_col_2_2 line 54
  47. lemma OAI.PencilAlgebra.low_col_2_3 line 55
  48. lemma OAI.PencilAlgebra.low_col_2_4 line 56
  49. lemma OAI.PencilAlgebra.low_col_2_5 line 57
  50. lemma OAI.PencilAlgebra.low_col_2_6 line 58
  51. lemma OAI.PencilAlgebra.low_col_2_7 line 59
  52. lemma OAI.PencilAlgebra.low_col_2_8 line 60
  53. lemma OAI.PencilAlgebra.low_col_2_9 line 61
  54. lemma OAI.PencilAlgebra.high_col_2_0 line 62
  55. lemma OAI.PencilAlgebra.high_col_2_1 line 63
  56. lemma OAI.PencilAlgebra.high_col_2_2 line 64
  57. lemma OAI.PencilAlgebra.high_col_2_3 line 65
  58. lemma OAI.PencilAlgebra.high_col_2_4 line 66
  59. lemma OAI.PencilAlgebra.high_col_2_5 line 67
  60. lemma OAI.PencilAlgebra.high_col_2_6 line 68
  61. lemma OAI.PencilAlgebra.high_col_2_7 line 69
  62. lemma OAI.PencilAlgebra.high_col_2_8 line 70
  63. lemma OAI.PencilAlgebra.high_col_2_9 line 71
  64. lemma OAI.PencilAlgebra.low_col line 72
  65. lemma OAI.PencilAlgebra.high_col line 104