OAI/Analysis/MatrixSigning/Realization/MatrixStructureRealization.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Realization.natLE line 10
  2. def OAI.CurrentKS.Realization.natEq line 14
  3. def OAI.CurrentKS.Realization.matrixEntry line 19
  4. def OAI.CurrentKS.Realization.Realizes.matrixTabulate line 28
  5. def OAI.CurrentKS.Realization.identityEntry line 44
  6. def OAI.CurrentKS.Realization.identityMatrix line 48
  7. lemma OAI.CurrentKS.Realization.identityMatrix_data line 56
  8. def OAI.CurrentKS.Realization.transposeData line 67
  9. def OAI.CurrentKS.Realization.transposeMatrix line 70
  10. lemma OAI.CurrentKS.Realization.transpose_data line 80
  11. def OAI.CurrentKS.Realization.matrixMulData line 91
  12. def OAI.CurrentKS.Realization.matrixMul line 94
  13. lemma OAI.CurrentKS.Realization.matrixMul_data line 102
  14. def OAI.CurrentKS.Realization.fromBlocksData line 109
  15. def OAI.CurrentKS.Realization.fromBlocks line 113
  16. lemma OAI.CurrentKS.Realization.ofFn_sum line 121
  17. lemma OAI.CurrentKS.Realization.fromBlocks_data line 126