Adjugate of charmatrix

Stream: Is there code for X?

[Roman Bacik]

I am having hard time with verifying the second theorem, which follows from the first one, since charmatrix has degree one elements only on diagonal:

import Mathlib

open Matrix Polynomial

theorem det_degree_le_sum_degrees {n : ℕ} [NeZero n] (M : Matrix (Fin n) (Fin n) ℤ[X]) :
    (M.det).natDegree ≤ ∑ i : Fin n, ∑ j : Fin n, (M j i).natDegree := by
  sorry

theorem adj_poly_degrees {n : ℕ} [NeZero n] (A : Matrix (Fin n) (Fin n) ℤ) :
    ∀ i j : Fin n,
    let p := (charmatrix A).adjugate i j
    (i = j → p.Monic ∧ p.natDegree = n - 1) ∧
    (i ≠ j → p.natDegree ≤ n - 2) := by
  sorry

I wonder if we have something similar. I have some partial implementation here as Lemma4 and Lemma6.

[Roman Bacik]

I have finally finished the formal proof here if anyone is interested.