Commit 2024-01-04 07:13 f61a485e

View on Github →

feat: move replaceVertex to its own file (#9400)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

deleted theorem SimpleGraph.adj_replaceVertex_iff_of_ne

deleted theorem SimpleGraph.adj_replaceVertex_iff_of_ne_left

deleted theorem SimpleGraph.adj_replaceVertex_iff_of_ne_right

deleted theorem SimpleGraph.not_adj_replaceVertex_same

deleted theorem SimpleGraph.replaceVertex_self

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

Created Mathlib/Combinatorics/SimpleGraph/Operations.lean

added theorem SimpleGraph.adj_replaceVertex_iff_of_ne

added theorem SimpleGraph.adj_replaceVertex_iff_of_ne_left

added theorem SimpleGraph.adj_replaceVertex_iff_of_ne_right

added theorem SimpleGraph.not_adj_replaceVertex_same

added theorem SimpleGraph.replaceVertex_self