∀ {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'), ((Matrix.reindex em en) A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular