OAI/Combinatorics/SecondNeighborhood/GenericRankGlobalMinors.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeymourSecondNeighborhood.Pruning.matrixLSupport line 14
2. def OAI.SeymourSecondNeighborhood.Pruning.matrixNTransposeSupport line 18
3. theorem OAI.SeymourSecondNeighborhood.Pruning.matrixLSupport_iff_leftCovers line 22
4. theorem OAI.SeymourSecondNeighborhood.Pruning.matrixNTransposeSupport_iff_rightCovers line 31
5. def OAI.SeymourSecondNeighborhood.Pruning.matrixLMatchingMinor line 36
6. def OAI.SeymourSecondNeighborhood.Pruning.matrixNTransposeMatchingMinor line 41
7. theorem OAI.SeymourSecondNeighborhood.Pruning.eval_matrixLMatchingMinor line 46
8. theorem OAI.SeymourSecondNeighborhood.Pruning.eval_matrixNTransposeMatchingMinor line 54
9. theorem OAI.SeymourSecondNeighborhood.Pruning.det_matrixLMatchingMinor_ne_zero line 63
10. theorem OAI.SeymourSecondNeighborhood.Pruning.det_matrixNTransposeMatchingMinor_ne_zero line 94