Commit 2024-02-13 12:46 c6636bb8

View on Github →

chore(SimpleGraph/Finite): drop some DecidableEq assumptions (#10441)

  • don't assume DecidableEq in card_edgeFinset_le_card_choose_two;
  • make edgeFinset_deleteEdges work with any Fintype G.edgeSet and Fintype (G.deleteEdges s).edgeSet instances;
  • don't assume DecidbaleEq in theorems about DeleteFar.

Estimated changes

modified theorem SimpleGraph.edgeFinset_top