eval_charpolyRev — Mathlib

English

Evaluating the reverse characteristic polynomial at 0 gives 1:

Русский

Значение обратно-характеристического многочлена при X = 0 равно 1.

LaTeX

$$$\\operatorname{eval}(0, M.\\mathrm{charpolyRev}) = 1$$$

Lean4

@[simp]
theorem eval_charpolyRev : eval 0 M.charpolyRev = 1 :=
  by
  rw [charpolyRev, ← coe_evalRingHom, RingHom.map_det, ← det_one (R := R) (n := n)]
  have : (1 - (X : R[X]) • M.map C).map (eval 0) = 1 := by ext i j;
    rcases eq_or_ne i j with hij | hij <;> simp [hij, one_apply]
  congr

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