Commit 2024-11-28 13:23 4b33b00f

View on Github →

feat: adjoining identity matrices to TU matrices (#19076)

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean

modified theorem Matrix.IsTotallyUnimodular.apply

added theorem Matrix.IsTotallyUnimodular.fromRows_unitlike

added theorem Matrix.IsTotallyUnimodular.reindex

modified theorem Matrix.IsTotallyUnimodular.submatrix

modified theorem Matrix.fromColumns_col0_isTotallyUnimodular_iff

added theorem Matrix.fromColumns_one_isTotallyUnimodular_iff

added theorem Matrix.fromRows_isTotallyUnimodular_iff_rows

added theorem Matrix.fromRows_one_isTotallyUnimodular_iff

modified theorem Matrix.fromRows_row0_isTotallyUnimodular_iff

deleted theorem Matrix.mapEquiv_isTotallyUnimodular

added theorem Matrix.one_fromColumns_isTotallyUnimodular_iff

added theorem Matrix.one_fromRows_isTotallyUnimodular_iff

added theorem Matrix.reindex_isTotallyUnimodular