OAI/Probability/SKRatio/Matrices/DetMultilinear.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioGaussian.LogDet.detMultilinear line 13
2. lemma OAI.SKRatioGaussian.LogDet.hasDerivAt_det_update line 17
3. lemma OAI.SKRatioGaussian.LogDet.det_updateRow_trace line 29
4. lemma OAI.SKRatioGaussian.LogDet.hasDerivAt_det_adjugate line 41
5. lemma OAI.SKRatioGaussian.LogDet.adjugate_eq_det_smul_inv line 46
6. lemma OAI.SKRatioGaussian.LogDet.hasDerivAt_det line 51
7. lemma OAI.SKRatioGaussian.LogDet.hasDerivAt_logdet line 58