OAI/Probability/StrongRayleigh/MixedDeterminant.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336AdditiveD139.det_fromBlocks_skew_nonneg_of_posDef line 14
2. theorem OAI.Problem336AdditiveD139.det_fromBlocks_skew_nonneg line 27
3. def OAI.Problem336AdditiveD139.mixedRowMatrix line 44
4. theorem OAI.Problem336AdditiveD139.mixedRowMatrix_det_nonneg line 48
5. theorem OAI.Problem336AdditiveD139.mixedRowMatrix_det_re_nonneg line 70
6. theorem OAI.Problem336AdditiveD139.mixedRowMatrix_det_im line 77