OAI/Analysis/MatrixSigning/Realization/ArrayRealization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.Realization.natIsZero line 12
2. def OAI.CurrentKS.Realization.lookupStep line 21
3. def OAI.CurrentKS.Realization.lookupStepRealizes line 24
4. lemma OAI.CurrentKS.Realization.lookupStep_zero line 35
5. lemma OAI.CurrentKS.Realization.lookupStep_getD line 41
6. def OAI.CurrentKS.Realization.getD line 54
7. lemma OAI.CurrentKS.Realization.fold_length line 63
8. def OAI.CurrentKS.Realization.lengthList line 68
9. def OAI.CurrentKS.Realization.Realizes.tabulate line 74
10. lemma OAI.CurrentKS.Realization.fold_natAdd line 80
11. def OAI.CurrentKS.Realization.natMul line 85
12. lemma OAI.CurrentKS.Realization.iterate_ratSucc line 94
13. def OAI.CurrentKS.Realization.natToRat line 99