mathlib
0f56b2df - feat(combinatorics/simple_graph/connectivity): simp confluence (#15153)

Commit
3 years ago
feat(combinatorics/simple_graph/connectivity): simp confluence (#15153) From branch `walks_and_trees`. Adds data/list/basic lemma to help simp prove `d ∈ p.reverse.darts ↔ d.symm ∈ p.darts`.
Author
Parents
Loading