OAI/Analysis/MatrixSigning/Realization/CleanRoutine.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.CleanRoutine.Word line 13
  2. def OAI.CurrentKS.CleanRoutine.io line 15
  3. lemma OAI.CurrentKS.CleanRoutine.io_zero line 17
  4. lemma OAI.CurrentKS.CleanRoutine.io_ne line 18
  5. structure OAI.CurrentKS.CleanRoutine.Routine line 20
  6. def OAI.CurrentKS.CleanRoutine.embedding line 25
  7. lemma OAI.CurrentKS.CleanRoutine.io_embedding line 28
  8. lemma OAI.CurrentKS.CleanRoutine.io_other line 31
  9. def OAI.CurrentKS.CleanRoutine.Routine.pad line 38
  10. def OAI.CurrentKS.CleanRoutine.Routine.compose line 45
  11. def OAI.CurrentKS.CleanRoutine.Routine.reindex line 54
  12. def OAI.CurrentKS.CleanRoutine.Routine.weaken line 61
  13. def OAI.CurrentKS.CleanRoutine.framing line 67
  14. def OAI.CurrentKS.CleanRoutine.transfer line 76
  15. lemma OAI.CurrentKS.CleanRoutine.transfer_spec line 80