OAI/Analysis/MatrixSigning/Realization/PencilCompileRealization.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Realization.matrixNegData line 13
  2. def OAI.CurrentKS.Realization.matrixSubData line 14
  3. def OAI.CurrentKS.Realization.matrixSub line 16
  4. lemma OAI.CurrentKS.Realization.matrixNeg_data line 18
  5. lemma OAI.CurrentKS.Realization.matrixSub_data line 21
  6. def OAI.CurrentKS.Realization.zeroRect line 25
  7. lemma OAI.CurrentKS.Realization.zeroRect_data line 32
  8. def OAI.CurrentKS.Realization.blockDiagonalData line 37
  9. def OAI.CurrentKS.Realization.blockDiagonal line 40
  10. lemma OAI.CurrentKS.Realization.blockDiagonal_data line 46
  11. def OAI.CurrentKS.Realization.basisData line 54
  12. def OAI.CurrentKS.Realization.basisVector line 55
  13. lemma OAI.CurrentKS.Realization.basis_data line 57
  14. def OAI.CurrentKS.Realization.pencilFromEvalData line 64
  15. def OAI.CurrentKS.Realization.Realizes.pencilFromEval line 68
  16. lemma OAI.CurrentKS.Realization.pencilFromEval_data line 83