Theorems · Theorem · linear algebra

Matrix.IsTotallyUnimodular.reindex

∀ {m : Type u_1} {m' : Type u_2} {n : Type u_3} {n' : Type u_4} {R : Type u_5} [inst : CommRing R] {A : Matrix m n R}
  (em : m ≃ m') (en : n ≃ n'), A.IsTotallyUnimodular → ((Matrix.reindex em en) A).IsTotallyUnimodular

Defined in

Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Cited by

1 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing