OAI/Combinatorics/SecondNeighborhood/MatrixMapsCommute.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SeymourSecondNeighborhood.Pruning.conflict_of_product_ne_zero line 12
2. theorem OAI.SeymourSecondNeighborhood.Pruning.matrixN_mul_matrixL_apply line 24
3. theorem OAI.SeymourSecondNeighborhood.Pruning.matrixA_mul_matrixB_apply line 64
4. theorem OAI.SeymourSecondNeighborhood.Pruning.matrixN_mul_matrixL_eq_matrixA_mul_matrixB line 104