mathlib3

d67c4697 - feat(combinatorics/simple_graph/basic): edge deletion (#11054)

feat(combinatorics/simple_graph/basic): edge deletion (#11054) Function to delete edges from a simple graph, and some associated lemmas. Also defines `sym2.to_rel` as an inverse to `sym2.from_rel`.