Commit 2026-07-20 03:19 b9a117e2
View on Github →chore(Combinatorics/SimpleGraph/Finite): fix Fintype instances in edgeFinset_inf (#41789)
Unlike edgeFinset_sup, edgeFinset_inf only accepts Fintype instances for G and H and not their inf, relying on the fintypeEdgeSetInf instance providing it.
This means the theorem can't be used with a different Fintype (G₁ ⊓ G₂).edgeSet.