∀ {m : Type u_2} {m' : Type u_6} (R : Type u_11) (A : Type u_12) [inst : Semiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : Module R A] [inst_3 : DecidableEq m] [inst_4 : DecidableEq m'] [inst_5 : One A] (e : m ≃ m'),
  (Matrix.reindexLinearEquiv R A e e) 1 = 1