English
The determinant of (I + r M) expands as 1 + (trace M) r + higher order terms in r; explicitly, det(I + r M) = 1 + (trace M) r + (det(I + X M)).divX.divX evaluated at r times r^2.
Русский
Разложение детерминанта по малому параметру r: det(I + r M) = 1 + (trace M) r + далее по r^2.
LaTeX
$$$$ \\det\\left(I + r M\\right) = 1 + \\operatorname{tr}(M) r + \\left( \\det\\left(I + X M\\right) \\right)_{\\div X}^{\\div X} r^2. $$$$
Lean4
theorem det_one_add_X_smul (M : Matrix n n R) :
det (1 + (X : R[X]) • M.map C) = (1 : R[X]) + trace M • X + (det (1 + (X : R[X]) • M.map C)).divX.divX * X ^ 2 :=
by
rw [Algebra.smul_def (trace M), ← C_eq_algebraMap, pow_two, ← mul_assoc, add_assoc, ← add_mul, ←
coeff_det_one_add_X_smul_one, ← coeff_divX, add_comm (C _), divX_mul_X_add, add_comm (1 : R[X]), ← C.map_one]
convert (divX_mul_X_add _).symm
rw [coeff_zero_eq_eval_zero, eval_det_add_X_smul, det_one, eval_one]
