Theorem SimpleGraph.edist_eq_zero_iff

Modification history

2026-05-21 10:51

Mathlib/Combinatorics/SimpleGraph/Metric.lean

feat(Combinatorics/SimpleGraph/Walk): make `p.Nil` the simpNF of `p = nil` and `p.length = 0` (#39218) …

Modified SimpleGraph.edist_eq_zero_iff View on Github →

2024-07-27 14:22

Mathlib/Combinatorics/SimpleGraph/Metric.lean

feat(Combinatorics/SimpleGraph): define `edist` and rewrite `dist` (#14582) …

Added SimpleGraph.edist_eq_zero_iff View on Github →