mathlib
99e8971d - refactor(combinatorics/simple_graph/connectivity): fix simp lemmas for `to_delete_edges`, use dot notation for `transfer` lemmas (#17644)

Commit
3 years ago
refactor(combinatorics/simple_graph/connectivity): fix simp lemmas for `to_delete_edges`, use dot notation for `transfer` lemmas (#17644) The definition of `to_delete_edges` was recently changed when `transfer` was introduced, and this inadvertently changed how the simp lemmas for `to_delete_edges` were defined syntactically. This change keeps the simp lemmas from switching `to_delete_edges` to `transfer`. This commit also switches `is_path` and `is_cycle` constructors for `transfer` use dot notation.
Author
Parents
Loading