Open teorth opened 5 hours ago
Only a generating set of implications needs to be added to Subgraph.lean, of course. Human-readable sketches of proofs can be added in comments.
Only a generating set of implications needs to be added to Subgraph.lean, of course. Human-readable sketches of proofs can be added in comments.