OAI/Analysis/Quantum/PPTSquare/Mod139Products.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ModularPencil.P139.B_V_row0 line 12
  2. lemma OAI.ModularPencil.P139.A_V_row0 line 13
  3. lemma OAI.ModularPencil.P139.B_V_row1 line 14
  4. lemma OAI.ModularPencil.P139.A_V_row1 line 15
  5. lemma OAI.ModularPencil.P139.B_V_row2 line 16
  6. lemma OAI.ModularPencil.P139.A_V_row2 line 17
  7. lemma OAI.ModularPencil.P139.B_V_row3 line 18
  8. lemma OAI.ModularPencil.P139.A_V_row3 line 19
  9. lemma OAI.ModularPencil.P139.B_V_row4 line 20
  10. lemma OAI.ModularPencil.P139.A_V_row4 line 21
  11. lemma OAI.ModularPencil.P139.B_V_row5 line 22
  12. lemma OAI.ModularPencil.P139.A_V_row5 line 23
  13. lemma OAI.ModularPencil.P139.B_V_row6 line 24
  14. lemma OAI.ModularPencil.P139.A_V_row6 line 25
  15. lemma OAI.ModularPencil.P139.B_V_row7 line 26
  16. lemma OAI.ModularPencil.P139.A_V_row7 line 27
  17. lemma OAI.ModularPencil.P139.B_V_row8 line 28
  18. lemma OAI.ModularPencil.P139.A_V_row8 line 29
  19. lemma OAI.ModularPencil.P139.B_V_row9 line 30
  20. lemma OAI.ModularPencil.P139.A_V_row9 line 31
  21. lemma OAI.ModularPencil.P139.B_V_row10 line 32
  22. lemma OAI.ModularPencil.P139.A_V_row10 line 33
  23. lemma OAI.ModularPencil.P139.B_V_row11 line 34
  24. lemma OAI.ModularPencil.P139.A_V_row11 line 35
  25. lemma OAI.ModularPencil.P139.B_V_row12 line 36
  26. lemma OAI.ModularPencil.P139.A_V_row12 line 37
  27. lemma OAI.ModularPencil.P139.B_V_row13 line 38
  28. lemma OAI.ModularPencil.P139.A_V_row13 line 39
  29. lemma OAI.ModularPencil.P139.B_V_row14 line 40
  30. lemma OAI.ModularPencil.P139.A_V_row14 line 41
  31. lemma OAI.ModularPencil.P139.B_V_row15 line 42
  32. lemma OAI.ModularPencil.P139.A_V_row15 line 43
  33. lemma OAI.ModularPencil.P139.B_V_row16 line 44
  34. lemma OAI.ModularPencil.P139.A_V_row16 line 45
  35. lemma OAI.ModularPencil.P139.B_V_row17 line 46
  36. lemma OAI.ModularPencil.P139.A_V_row17 line 47
  37. lemma OAI.ModularPencil.P139.B_V_row18 line 48
  38. lemma OAI.ModularPencil.P139.A_V_row18 line 49
  39. lemma OAI.ModularPencil.P139.B_V_row19 line 50
  40. lemma OAI.ModularPencil.P139.A_V_row19 line 51
  41. lemma OAI.ModularPencil.P139.B_V line 52
  42. lemma OAI.ModularPencil.P139.step line 75
  43. lemma OAI.ModularPencil.P139.final line 101
  44. lemma OAI.ModularPencil.P139.f_def line 102
  45. lemma OAI.ModularPencil.P139.charpoly_A line 105
  46. lemma OAI.ModularPencil.P139.charpoly line 108