taylor expansion of determinant

Stream: Is there code for X?

[Andrew Yang]

Do we have the taylor-like expansion of $\operatorname{det}(I + xA)$? In particular I only need the following

import Mathlib

lemma Matrix.det_one_add_smul {n} [Fintype n] [DecidableEq n] {R} [CommRing R] (M : Matrix n n R) (r : R) :
    ∃ s : R, det (1 + r • M : Matrix n n R) = (1 + r • trace M + r ^ 2 * s : R) := sorry

[Eric Wieser]

This was on my TODO list in lean-matrix-cookbook, but I never got to spending any time on it

[Andrew Yang]

I managed to get the following

import Mathlib

open Polynomial in
lemma Matrix.eval_det_add_X_smul {n} {R} [CommRing R] (A) (M : Matrix (Fin n) (Fin n) R) :
    (det (A + (X : R[X]) • M.map C : Matrix (Fin n) (Fin n) R[X])).eval 0 = (det A).eval 0 := by
  simp only [eval_det, map_zero, map_add, eval_add, Algebra.smul_def, _root_.map_mul]
  simp only [algebraMap_eq_smul, matPolyEquiv_smul_one, map_X, X_mul, eval_mul_X, mul_zero,
    add_zero]

lemma Matrix.trace_submatrix_succ {n : ℕ} {R} [CommRing R] (M : Matrix (Fin n.succ) (Fin n.succ) R) :
    M 0 0 + trace (submatrix M Fin.succ Fin.succ) = trace M := by
  delta trace
  rw [← (finSuccEquiv n).symm.sum_comp]
  simp

open Polynomial in
lemma Matrix.det_one_add_smul_aux {n} {R} [CommRing R] (M : Matrix (Fin n) (Fin n) R) :
    (derivative <| det (1 + (X : R[X]) • M.map C)).eval 0 = trace M := by
  induction n with
  | zero => simp
  | succ n IH =>
    rw [det_succ_row_zero, map_sum, eval_finset_sum]
    simp only [add_apply, smul_apply, map_apply, smul_eq_mul, X_mul_C, submatrix_add,
      submatrix_smul, Pi.add_apply, Pi.smul_apply, submatrix_map, derivative_mul, map_add,
      derivative_C, zero_mul, derivative_X, mul_one, zero_add, eval_add, eval_mul, eval_C, eval_X,
      mul_zero, add_zero, eval_det_add_X_smul, eval_pow, eval_neg, eval_one]
    rw [Finset.sum_eq_single 0]
    · simp only [Fin.val_zero, pow_zero, derivative_one, eval_zero, one_apply_eq, eval_one,
        mul_one, zero_add, one_mul, Fin.succAbove_zero, submatrix_one _ (Fin.succ_injective _),
        det_one, IH, trace_submatrix_succ]
    · intro i _ hi
      cases n with
      | zero => exact (hi (Subsingleton.elim i 0)).elim
      | succ n =>
        simp only [one_apply_ne' hi, eval_zero, mul_zero, zero_add, zero_mul, add_zero]
        rw [det_eq_zero_of_column_eq_zero 0, eval_zero, mul_zero]
        intro j
        rw [submatrix_apply, Fin.succAbove_below, one_apply_ne]
        · exact (bne_iff_ne (Fin.succ j) (Fin.castSucc 0)).mp rfl
        · rw [Fin.castSucc_zero]; exact lt_of_le_of_ne (Fin.zero_le _) hi.symm
    · exact fun H ↦ (H <| Finset.mem_univ _).elim