eval_det_add_X_smul — Mathlib

English

Adding a polynomial multiple of X to a polynomial matrix does not change the evaluation of the determinant at 0.

Русский

Добавление полиномного множителя X к полиномной матрице не меняет значение детерминанта при оценке в 0.

LaTeX

$$$\\big(\\det\\big(A + X\\cdot M.map C\\big)\\big).\\mathrm{eval}\\,0 = \\det A.\\mathrm{eval}\\,0$$$

Lean4

theorem eval_det_add_X_smul {R : Type*} [CommRing R] (A : Matrix n n R[X]) (M : Matrix n n R) :
    (det (A + (X : R[X]) • M.map C)).eval 0 = (det A).eval 0 :=
  by
  simp only [eval_det, map_zero, map_add, eval_add, Algebra.smul_def, map_mul]
  simp only [Algebra.algebraMap_eq_smul_one, matPolyEquiv_smul_one, map_X, X_mul, eval_mul_X, mul_zero, add_zero]

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