OAI/Analysis/MatrixSigning/Realization/CoordinateRealization.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Realization.natLT line 11
  2. def OAI.CurrentKS.Realization.Realizes.scaleMatrix line 15
  3. def OAI.CurrentKS.Realization.negateMatrix line 20
  4. def OAI.CurrentKS.Realization.zeroMatrix line 24
  5. def OAI.CurrentKS.Realization.reEntryData line 29
  6. def OAI.CurrentKS.Realization.reEntry line 32
  7. def OAI.CurrentKS.Realization.imEntryData line 42
  8. def OAI.CurrentKS.Realization.imEntry line 46
  9. def OAI.CurrentKS.Realization.squareTabData line 57
  10. def OAI.CurrentKS.Realization.squareTabulate line 60
  11. def OAI.CurrentKS.Realization.realDecodeData line 67
  12. def OAI.CurrentKS.Realization.realDecode line 72
  13. lemma OAI.CurrentKS.Realization.reEntry_data line 77
  14. lemma OAI.CurrentKS.Realization.imEntry_data line 86
  15. lemma OAI.CurrentKS.Realization.squareTab_data line 93
  16. lemma OAI.CurrentKS.Realization.realDecode_data line 98