## Construction of a Flow Equivalent Forest in Lean 4

### Setup

- Install
`elan`

. - Run
`lake exe cache get`

to not compile`mathlib4`

yourself. - Run
`lake build`

to check the project.

### Theorem

For an undirected flow network *flow matrix* to be the matrix

For all

In particular, given a matrix

The main result of our project is the construction of the acyclic network for a given matrix, see `FlowEquivalentForest/Flow/Matrix.lean`

.

### Bibliography

- Gomory, Ralph E., and Tien Chung Hu. "Multi-terminal network flows."
*Journal of the Society for Industrial and Applied Mathematics*9.4 (1961): 551-570.