Skip to content

Commit aef322b

Browse files
committed
feat(Combinatorics/SimpleGraph): split Walk.lean into 5 files (#31573)
Split into 5 files in a new `Walks` subfolder: - `Basic.lean`: basic definitions and theorems about them, without modifying the walks: `Walk`, `Nil`, `length`, `support`, `darts`, `edges`, `edgeSet` - `Traversal.lean`: access parts of a walk: `getVert`, `snd`, `penultimate`, `firstDart`, `lastDart` - `Operations.lean`: similar to the existing `WalkDecomp.lean`, this file defines operations on walks: `copy`, `append`, `concat`, `reverse`, `drop`, `take`, `tail`, `dropLast`. The name of the file matches `SimpleGraph/Operations.lean` which defines operations on graphs. - `Maps.lean`: operations that map the walk to another graph: `map`, `mapLe`, `transfer`, `induce`, `toDeleteEdges`, `toDeleteEdge`. The name of the file matches `SimpleGraph/Maps.lean` which defines maps on graphs. - `Subwalks.lean`: the definition of `IsSubwalk` and theorems about it Deprecates the original `Walk.lean` module.
1 parent 4322ca4 commit aef322b

File tree

9 files changed

+1666
-1521
lines changed

9 files changed

+1666
-1521
lines changed

Mathlib.lean

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3212,6 +3212,11 @@ public import Mathlib.Combinatorics.SimpleGraph.Turan
32123212
public import Mathlib.Combinatorics.SimpleGraph.Tutte
32133213
public import Mathlib.Combinatorics.SimpleGraph.UniversalVerts
32143214
public import Mathlib.Combinatorics.SimpleGraph.Walk
3215+
public import Mathlib.Combinatorics.SimpleGraph.Walks.Basic
3216+
public import Mathlib.Combinatorics.SimpleGraph.Walks.Maps
3217+
public import Mathlib.Combinatorics.SimpleGraph.Walks.Operations
3218+
public import Mathlib.Combinatorics.SimpleGraph.Walks.Subwalks
3219+
public import Mathlib.Combinatorics.SimpleGraph.Walks.Traversal
32153220
public import Mathlib.Combinatorics.Young.SemistandardTableau
32163221
public import Mathlib.Combinatorics.Young.YoungDiagram
32173222
public import Mathlib.Computability.Ackermann

Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Kyle Miller, Pim Otte
55
-/
66
module
77

8-
public import Mathlib.Combinatorics.SimpleGraph.Walk
8+
public import Mathlib.Combinatorics.SimpleGraph.Walks.Operations
99

1010
/-!
1111
# Decomposing walks

Mathlib/Combinatorics/SimpleGraph/Paths.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@ Authors: Kyle Miller
66
module
77

88
public import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
9-
public import Mathlib.Combinatorics.SimpleGraph.Walk
9+
public import Mathlib.Combinatorics.SimpleGraph.Walks.Maps
10+
public import Mathlib.Combinatorics.SimpleGraph.Walks.Subwalks
1011

1112
/-!
1213

0 commit comments

Comments
 (0)