TU matrix API

Stream: mathlib4

[Martin Dvořák]

I often work with the API for totally unimodular matrices.

It turns out that this proof part
https://github.com/leanprover-community/mathlib4/blob/708ea06c33feeced7befb2cc175aa048852df2ab/Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean#L45-L53
is useful for me as a separate lemma.

The proof of the lemma (with some further decomposition into reüsable parts) is here:
https://github.com/Ivan-Sergeyev/seymour/blob/fa9680ed1e746fe392b2e4eed753d548ae06ee92/Seymour/Matrix/TotalUnimodularityViolation.lean#L12-L37

Do you want it decomposed my way in Mathlib? If so, which file should it go to?