OAI/Analysis/FreeWords/MatrixTraceL2.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.KKMatrixL2.norm_trace_le_traceNormline 31 - theorem
OAI.KKMatrixL2.matrix_trace_l2_nullline 39
OAI/Analysis/FreeWords/MatrixTraceL2.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.KKMatrixL2.norm_trace_le_traceNorm line 31OAI.KKMatrixL2.matrix_trace_l2_null line 39