OAI/Analysis/MatrixSigning/Complexity/PolynomialOriginalFields.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CurrentKS.Realization.poly_originalView line 13
2. instance OAI.CurrentKS.Realization.poly_originalD line 14
3. instance OAI.CurrentKS.Realization.poly_originalRecords line 15
4. instance OAI.CurrentKS.Realization.poly_originalN line 16
5. instance OAI.CurrentKS.Realization.poly_recordEntry line 17
6. instance OAI.CurrentKS.Realization.poly_recordCoordinate line 18
7. instance OAI.CurrentKS.Realization.poly_recordCoordinates line 19
8. instance OAI.CurrentKS.Realization.poly_originalRecord line 20
9. instance OAI.CurrentKS.Realization.poly_originalCoordinates line 21
10. instance OAI.CurrentKS.Realization.poly_recordTrace line 22
11. instance OAI.CurrentKS.Realization.poly_originalTrace line 23
12. instance OAI.CurrentKS.Realization.poly_originalTraces line 24
13. instance OAI.CurrentKS.Realization.poly_originalScale line 25
14. instance OAI.CurrentKS.Realization.poly_originalOrientation line 26
15. instance OAI.CurrentKS.Realization.poly_nonzeroIndices line 27
16. instance OAI.CurrentKS.Realization.poly_originalIndices line 28
17. instance OAI.CurrentKS.Realization.poly_originalCountRealizes line 29
18. instance OAI.CurrentKS.Realization.poly_originalIndex line 30
19. instance OAI.CurrentKS.Realization.poly_originalNormalizedMatrix line 31
20. instance OAI.CurrentKS.Realization.poly_originalFaceRealizes line 32