Commit 2025-10-28 10:18 e3a51e40

View on Github →

feat(SimpleGraph): characterise when SimpleGraph V is a subsingleton/nontrivial (#30137) Helper lemmas I found useful in mutliple PRs for dispatching trivial cases.

Estimated changes