derivative_det_one_add_X_smul — Mathlib

English

See 130158 for the precise bound on natDegree of charmatrix entries.

Русский

См. 130158 для точной границы natDegree элементов charmatrix.

LaTeX

$$$$ \\operatorname{natDegree}(\\operatorname{charmatrix}(M)_{ij}) \\le (i = j) ? 1 : 0. $$$$

Lean4

/-- The derivative of `det (1 + M X)` at `0` is the trace of `M`. -/
theorem derivative_det_one_add_X_smul (M : Matrix n n R) :
    (derivative <| det (1 + (X : R[X]) • M.map C)).eval 0 = trace M :=
  by
  let e := Matrix.reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
  rw [← Matrix.det_reindexLinearEquiv_self R[X] (Fintype.equivFin n)]
  convert derivative_det_one_add_X_smul_aux (e M)
  · ext; simp [map_add, e]
  · delta trace
    rw [← (Fintype.equivFin n).symm.sum_comp]
    simp_rw [e, reindexLinearEquiv_apply, reindex_apply, diag_apply, submatrix_apply]

Похожие утверждения