OAI/Analysis/BiholderTransport/LinearAlgebra/DeterminantOrder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.det_one_add_posSemidef_ge_one line 19
2. lemma OAI.WeakMTWTransport.det_le_of_posDef_le line 41
3. lemma OAI.WeakMTWTransport.det_one_add_vecMulVec line 72
4. lemma OAI.WeakMTWTransport.congruence_rank_one line 81
5. lemma OAI.WeakMTWTransport.oblique_fixes_kernel_form line 86
6. lemma OAI.WeakMTWTransport.transpose_congruence_mono line 99