OAI/Analysis/MatrixSigning/Realization/OriginalFieldsRealization.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Realization.fieldValues line 15
  2. lemma OAI.CurrentKS.Realization.fieldValues_eq line 17
  3. lemma OAI.CurrentKS.Realization.fieldValues_get line 22
  4. abbrev OAI.CurrentKS.Realization.originalDataCode line 36
  5. def OAI.CurrentKS.Realization.originalData line 37
  6. def OAI.CurrentKS.Realization.originalCode line 38
  7. def OAI.CurrentKS.Realization.originalView line 39
  8. def OAI.CurrentKS.Realization.originalD line 41
  9. def OAI.CurrentKS.Realization.originalRecords line 42
  10. def OAI.CurrentKS.Realization.originalN line 44
  11. abbrev OAI.CurrentKS.Realization.recordCode line 47
  12. abbrev OAI.CurrentKS.Realization.recordPointCode line 48
  13. def OAI.CurrentKS.Realization.recordEntryData line 50
  14. def OAI.CurrentKS.Realization.recordEntry line 53
  15. def OAI.CurrentKS.Realization.recordCoordinateData line 63
  16. def OAI.CurrentKS.Realization.recordCoordinate line 65
  17. def OAI.CurrentKS.Realization.recordCoordinatesData line 72
  18. def OAI.CurrentKS.Realization.recordCoordinates line 74
  19. lemma OAI.CurrentKS.Realization.recordCoordinate_data line 77
  20. lemma OAI.CurrentKS.Realization.recordCoordinates_data line 89
  21. def OAI.CurrentKS.Realization.originalRecord line 93
  22. def OAI.CurrentKS.Realization.originalCoordinates line 100