Commit 2025-12-01 17:55 c5797bd5

View on Github →

feat(Combinatorics/SimpleGraph): use Sym2.diagSet instead of explicit sets (#32255)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

modified theorem SimpleGraph.edgeSet_eq_iff

modified theorem SimpleGraph.edgeSet_fromEdgeSet

modified theorem SimpleGraph.edgeSet_subset_setOf_not_isDiag

modified theorem SimpleGraph.edgeSet_top

modified theorem SimpleGraph.fromEdgeSet_not_isDiag

Modified Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

Modified Mathlib/Data/Sym/Card.lean

added theorem Sym2.card_diagSet_compl

Modified Mathlib/Data/Sym/Sym2.lean