Mathlib Changelog
v4
Changelog
About
Github
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