Commit 2024-05-21 09:57 af03206c
View on Github →refactor(SimpleGraph): Review deleteEdges (#11613)
Redefine SimpleGraph.deleteEdges in an order theory-friendly way, as was discussed several times. Refactor proofs to leverage the new definition and drop lemmas that are now direct consequences of other ones in order to make the API more modular.