Mathlib Changelog
v4
Changelog
About
Github
Theorem
SimpleGraph.reachable_eq_reflTransGen
Modification history
2025-12-09 05:22
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
feat(Combinatorics/SimpleGraph/Connectivity/Connected): a few lemmas about `Reachable` (#30570)
Added
SimpleGraph.reachable_eq_reflTransGen
View on Github →