Mathlib Changelog
v4
Changelog
About
Github
Theorem
SimpleGraph.fromEdgeSet_not_isDiag
Modification history
2025-12-01 17:55
Mathlib/Combinatorics/SimpleGraph/Basic.lean
feat(Combinatorics/SimpleGraph): use `Sym2.diagSet` instead of explicit sets (#32255)
Modified
SimpleGraph.fromEdgeSet_not_isDiag
View on Github →
2025-11-13 20:22
Mathlib/Combinatorics/SimpleGraph/Basic.lean
feat: the graph made of all non-diag edges is complete (#31443)
Added
SimpleGraph.fromEdgeSet_not_isDiag
View on Github →