coeff_det_one_add_X_smul_one — Mathlib

English

The derivative of det(1 + (X) • M.map C) evaluated at zero equals the trace of M.

Русский

Производная det(1 + X • M) в точке X = 0 равна trace(M).

LaTeX

$$$$ \\left. \\frac{d}{dX} \\det\\left(1 + X \\cdot M\pmatrix{M}\\right) \\right|_{X=0} = \\operatorname{tr}(M). $$$$

Lean4

theorem coeff_det_one_add_X_smul_one (M : Matrix n n R) : (det (1 + (X : R[X]) • M.map C)).coeff 1 = trace M := by
  simp only [← derivative_det_one_add_X_smul, ← coeff_zero_eq_eval_zero, coeff_derivative, zero_add, Nat.cast_zero,
    mul_one]

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