OAI/Combinatorics/SecondNeighborhood/KernelIndependence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SeymourSecondNeighborhood.Pruning.kernelB_vanishes_at_matched_left line 17
2. theorem OAI.SeymourSecondNeighborhood.Pruning.matrixB_lifts_linearIndependent line 28
3. theorem OAI.SeymourSecondNeighborhood.Pruning.matrixB_lift_mem_ker_matrixA line 52
4. theorem OAI.SeymourSecondNeighborhood.Pruning.card_le_finrank_ker_matrixA_of_lifts line 63
5. theorem OAI.SeymourSecondNeighborhood.Pruning.card_add_rank_matrixN_mul_matrixL_le_card_H_of_lifts line 86