Theorem SimpleGraph.Connected.diff_dist_adj

Modification history

2026-07-15 16:59
Mathlib/Combinatorics/SimpleGraph/Metric.lean
chore: delete deprecated declarations to the end of 2025 (#41178) …
Deleted SimpleGraph.Connected.diff_dist_adjView on Github →
2026-01-18 15:55
Mathlib/Combinatorics/SimpleGraph/Metric.lean
fix: add missing deprecations (#34087) …
Added SimpleGraph.Connected.diff_dist_adjView on Github →
2025-12-11 21:26
Mathlib/Combinatorics/SimpleGraph/Metric.lean
feat(Combinatorics/SimpleGraph/Acyclic): `IsAcyclic` -> `IsBipartite` (#32568) …
Deleted SimpleGraph.Connected.diff_dist_adjView on Github →
2025-09-28 13:29
Mathlib/Combinatorics/SimpleGraph/Metric.lean
feat(Combinatorics/SimpleGraph): add theorem `SimpleGraph.Connected.diff_dist_adj` (#27468) …
Added SimpleGraph.Connected.diff_dist_adjView on Github →