OAI/Probability/SpanningForest/CodedIncidenceMinors.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem336.FiniteIncidence.edgeAdj_comp_equiv line 14
  2. theorem OAI.Problem336.FiniteIncidence.connected_comp_equiv line 24
  3. theorem OAI.Problem336.FiniteIncidence.squareReducedGradient_det_sq_eq_connected line 32
  4. theorem OAI.Problem336.FiniteIncidence.squareReducedGradient_det_sq_eq_treeOn line 42
  5. def OAI.Problem336.FiniteIncidence.selectedEdges line 58
  6. theorem OAI.Problem336.FiniteIncidence.selectedEdges_subset line 61
  7. theorem OAI.Problem336.FiniteIncidence.selectedEdges_card line 67
  8. def OAI.Problem336.FiniteIncidence.selectedEdgeEquiv line 70
  9. theorem OAI.Problem336.FiniteIncidence.connected_restrict_iff_selectedEdges line 84
  10. theorem OAI.Problem336.FiniteIncidence.connected_restrict_iff_treeOn line 102
  11. theorem OAI.Problem336.FiniteIncidence.selectedEdges_card_add_one line 113
  12. theorem OAI.Problem336.FiniteIncidence.columnMinor_det_sq_eq_treeOn line 122