Commit 2025-05-06 05:41 58d83afb

View on Github →

fix(SimpleGraph): drop some DecidableEq assumptions (#24623)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Bipartite.lean

modified theorem SimpleGraph.isBipartiteWith_sum_degrees_eq_twice_card_edges

Modified Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

modified theorem SimpleGraph.map_edgeFinset_induce

modified theorem SimpleGraph.map_neighborFinset_induce