OAI/Probability/SpanningForest/IncidenceMinorClassification.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336.IncidenceMinor.connected_iff_root_reachable line 18
2. theorem OAI.Problem336.IncidenceMinor.reducedGradient_det_ne_zero line 31
3. theorem OAI.Problem336.IncidenceMinor.reducedGradient_det_eq_zero line 39
4. theorem OAI.Problem336.IncidenceMinor.reducedGradient_det_ne_zero_iff line 49
5. theorem OAI.Problem336.IncidenceMinor.reducedGradient_det_sq_eq_indicator line 58
6. theorem OAI.Problem336.IncidenceMinor.selected_minor_det_sq_eq_indicator line 76
7. theorem OAI.Problem336.IncidenceMinor.weightedLaplacian_connected_list_partition line 84