OAI/Analysis/MatrixSigning/Matrices/MatrixRealSmul.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.matrix_real_smul_zero line 15
2. lemma OAI.CurrentKS.matrix_real_smul_sum line 17
3. lemma OAI.CurrentKS.matrix_real_smul_smul line 20
4. lemma OAI.CurrentKS.opNorm_real_smul line 23
5. lemma OAI.CurrentKS.coe_S line 26
6. lemma OAI.CurrentKS.coe_varianceH line 29