OAI/Analysis/MatrixSigning/Realization/FaceArrayRealization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CurrentKS.Realization.indicesCode line 10
2. def OAI.CurrentKS.Realization.activeData line 12
3. def OAI.CurrentKS.Realization.activeIndices line 14
4. lemma OAI.CurrentKS.Realization.range_finRange line 21
5. lemma OAI.CurrentKS.Realization.activeData_data line 22
6. abbrev OAI.CurrentKS.Realization.extendDataCode line 31
7. def OAI.CurrentKS.Realization.extendEntryData line 32
8. def OAI.CurrentKS.Realization.extendEntry line 36
9. def OAI.CurrentKS.Realization.extendData line 52
10. def OAI.CurrentKS.Realization.extendVector line 54
11. lemma OAI.CurrentKS.Realization.extendEntry_data line 58
12. lemma OAI.CurrentKS.Realization.extendData_data line 74
13. lemma OAI.CurrentKS.Realization.activeIndex_data line 83