OAI/Analysis/MatrixSigning/Matrices/InnerRight.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Hermitian.inner_right_one line 16
2. lemma OAI.CurrentKS.Hermitian.hasDerivAt_inner_curve line 19
3. lemma OAI.CurrentKS.Hermitian.inverse_trace_stationarity line 27
4. lemma OAI.CurrentKS.Hermitian.sandwich_add line 44
5. lemma OAI.CurrentKS.Hermitian.sandwich_smul line 50
6. lemma OAI.CurrentKS.Hermitian.sandwich_inverse_cancel line 56
7. lemma OAI.CurrentKS.Hermitian.sandwich_pd line 65
8. lemma OAI.CurrentKS.Hermitian.pd_sum_scalar line 71
9. lemma OAI.CurrentKS.Hermitian.trace_zero_psd line 77