OAI/Analysis/MatrixSigning/Matrices/DenseRatMatrix.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KS.W07.DenseRatMatrix line 7
2. def OAI.KS.W07.DenseRatMatrix.decode line 11
3. def OAI.KS.W07.DenseRatMatrix.ofMatrix line 14
4. theorem OAI.KS.W07.DenseRatMatrix.decode_ofMatrix line 17
5. theorem OAI.KS.W07.DenseRatMatrix.ofMatrix_decode line 23
6. def OAI.KS.W07.decodeRatVector line 34
7. theorem OAI.KS.W07.decodeRatVector_ofFn line 36