∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {M : Matrix n n R}
  {I : Ideal R}, (∀ (i j : n), M i j ∈ I) → ∀ (k : ℕ), M.charpoly.coeff k ∈ I ^ (Fintype.card n - k)