det_one_add_smul — Mathlib

English

For any matrix M, the k-th power M^k equals evaluation of M under the polynomial X^k modulo the characteristic polynomial: M^k = aeval_M(X^k mod M.charpoly).

Русский

Для любой M верно: M^k = aeval_M(X^k modulo M.charpoly).

LaTeX

$$$$ M^{k} = \\operatorname{aeval}_{M}\\left( X^{k} \\bmod M^{\\text{charpoly}} \\right). $$$$

Lean4

/-- The first two terms of the Taylor expansion of `det (1 + r • M)` at `r = 0`. -/
theorem det_one_add_smul (r : R) (M : Matrix n n R) :
    det (1 + r • M) = 1 + trace M * r + (det (1 + (X : R[X]) • M.map C)).divX.divX.eval r * r ^ 2 := by
  simpa [eval_det, ← smul_eq_mul_diagonal] using congr_arg (eval r) (Matrix.det_one_add_X_smul M)

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