def Matrix.shortTableauPivot {X Y F : Type} [Field F] [DecidableEq X] [DecidableEq Y] (A : Matrix X Y F) (x : X) (y : Y) : Matrix X Y F

The result of the pivot operation in a short tableau (without exchanging the indices that define the pivot). This definition makes sense only if A x y is nonzero.

Equations

• A.shortTableauPivot x y = Matrix.of fun (i : X) (j : Y) => if j = y then if i = x then 1 / A x y else -A i y / A x y else if i = x then A x j / A x y else A i j - A i y * A x j / A x y

theorem Matrix.shortTableauPivot_row_pivot {X Y F : Type} [Field F] [DecidableEq X] [DecidableEq Y] (A : Matrix X Y F) (x : X) (y : Y) : A.shortTableauPivot x y x = fun (j : Y) => if j = y then 1 / A x y else A x j / A x y

theorem Matrix.shortTableauPivot_row_other {X Y F : Type} [Field F] [DecidableEq X] [DecidableEq Y] (A : Matrix X Y F) (x : X) (y : Y) (i : X) (hix : i ≠ x) : A.shortTableauPivot x y i = fun (j : Y) => if j = y then -A i y / A x y else A i j - A i y * A x j / A x y

theorem Matrix.IsTotallyUnimodular.shortTableauPivot {X Y F : Type} [DecidableEq X] [DecidableEq Y] [Field F] {A : Matrix X Y F} (hA : A.IsTotallyUnimodular) {x : X} {y : Y} (hxy : A x y ≠ 0) : (A.shortTableauPivot x y).IsTotallyUnimodular

Pivoting preserves total unimodularity.