OAI/Probability/SpanningForest/CauchyBinet.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem336.CauchyBinet.coeff_det_one_add_X_smul_card line 15
  2. theorem OAI.Problem336.CauchyBinet.det_one_add_X_mul_comm line 32
  3. theorem OAI.Problem336.CauchyBinet.det_mul_eq_sum_principal_minors line 38
  4. theorem OAI.Problem336.CauchyBinet.det_mul_transpose_eq_sum_principal_minors line 45
  5. abbrev OAI.Problem336.CauchyBinet.ColumnSets line 52
  6. def OAI.Problem336.CauchyBinet.columnIndexEquiv line 55
  7. def OAI.Problem336.CauchyBinet.columnMinor line 60
  8. theorem OAI.Problem336.CauchyBinet.columnMinor_map line 65
  9. theorem OAI.Problem336.CauchyBinet.columnMinor_map_det line 70
  10. theorem OAI.Problem336.CauchyBinet.det_mul_eq_sum_minors line 76
  11. theorem OAI.Problem336.CauchyBinet.det_mul_transpose_eq_sum_sq_minors line 88
  12. theorem OAI.Problem336.CauchyBinet.columnMinor_mul_diagonal line 99
  13. theorem OAI.Problem336.CauchyBinet.det_weighted_gram_eq_sum_sq_minors line 106
  14. theorem OAI.Problem336.CauchyBinet.det_weighted_gram_eq_sum_of_sq_minors line 119
  15. theorem OAI.Problem336.CauchyBinet.det_weighted_gram_eq_sum_filter line 137
  16. theorem OAI.Problem336.CauchyBinet.det_weighted_gram_map_eq_sum_filter line 146