Commit 2024-04-01 16:53 9d0b2332
View on Github →refactor: move SimpleGraph.Iso.card_edgeFinset_eq to untangle imports (#11817)
The single and currently unused theorem card_edgeFinset_eq in Combinatorics.SimpleGraph.Maps causes a dependency of that file on Combinatorics.SimpleGraph.Finite, which is problematic because the key concepts of Maps don't depend on graph finiteness at all. This commit moves the offending theorem to Operations in anticipation of #9317.