OAI/Probability/SpanningForest/WeightedCauchyBinet.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336.WeightedCauchyBinet.det_mul_expansion line 16
2. theorem OAI.Problem336.WeightedCauchyBinet.ordered_cauchy_binet line 30
3. theorem OAI.Problem336.WeightedCauchyBinet.weighted_gram_det line 62
4. theorem OAI.Problem336.WeightedCauchyBinet.weighted_gram_det_real line 81
5. theorem OAI.Problem336.WeightedCauchyBinet.det_submatrix_eq_zero_of_not_injective line 94
6. theorem OAI.Problem336.WeightedCauchyBinet.weighted_gram_det_injective line 99
7. theorem OAI.Problem336.WeightedCauchyBinet.weighted_gram_det_nonneg line 114
8. theorem OAI.Problem336.WeightedCauchyBinet.weighted_gram_det_pos line 123