OAI/Analysis/Quantum/PPTSquare/MatrixInverse.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PencilAlgebra.H_Hinv_row0 line 9
  2. lemma OAI.PencilAlgebra.H_C_row0 line 10
  3. lemma OAI.PencilAlgebra.H_Hinv_row1 line 11
  4. lemma OAI.PencilAlgebra.H_C_row1 line 12
  5. lemma OAI.PencilAlgebra.H_Hinv_row2 line 13
  6. lemma OAI.PencilAlgebra.H_C_row2 line 14
  7. lemma OAI.PencilAlgebra.H_Hinv_row3 line 15
  8. lemma OAI.PencilAlgebra.H_C_row3 line 16
  9. lemma OAI.PencilAlgebra.H_Hinv_row4 line 17
  10. lemma OAI.PencilAlgebra.H_C_row4 line 18
  11. lemma OAI.PencilAlgebra.H_Hinv_row5 line 19
  12. lemma OAI.PencilAlgebra.H_C_row5 line 20
  13. lemma OAI.PencilAlgebra.H_Hinv_row6 line 21
  14. lemma OAI.PencilAlgebra.H_C_row6 line 22
  15. lemma OAI.PencilAlgebra.H_Hinv_row7 line 23
  16. lemma OAI.PencilAlgebra.H_C_row7 line 24
  17. lemma OAI.PencilAlgebra.H_Hinv_row8 line 25
  18. lemma OAI.PencilAlgebra.H_C_row8 line 26
  19. lemma OAI.PencilAlgebra.H_Hinv_row9 line 27
  20. lemma OAI.PencilAlgebra.H_C_row9 line 28
  21. lemma OAI.PencilAlgebra.H_Hinv_row10 line 29
  22. lemma OAI.PencilAlgebra.H_C_row10 line 30
  23. lemma OAI.PencilAlgebra.H_Hinv_row11 line 31
  24. lemma OAI.PencilAlgebra.H_C_row11 line 32
  25. lemma OAI.PencilAlgebra.H_Hinv_row12 line 33
  26. lemma OAI.PencilAlgebra.H_C_row12 line 34
  27. lemma OAI.PencilAlgebra.H_Hinv_row13 line 35
  28. lemma OAI.PencilAlgebra.H_C_row13 line 36
  29. lemma OAI.PencilAlgebra.H_Hinv_row14 line 37
  30. lemma OAI.PencilAlgebra.H_C_row14 line 38
  31. lemma OAI.PencilAlgebra.H_Hinv line 39
  32. lemma OAI.PencilAlgebra.H_C line 57