∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] [inst_2 : Fintype n] {M : Matrix n n R},
  M ∈ Set.range ⇑(Matrix.scalar n) ↔ ∀ (t : Matrix.TransvectionStruct n R), Commute t.toMatrix M