English
Evaluating a polynomial matrix M at r yields a scalar polynomial det that matches the determinant after applying matPolyEquiv.
Русский
Оценка матрицы-полиномов M в r даёт скалярный полином, совпадающий с определителем после применения matPolyEquiv.
LaTeX
$$$\\mathrm{Polynomial.eval}\\; r\\; M.\\mathrm{det} = (\\mathrm{Polynomial.eval}\\; (\\mathrm{scalar}\\; n\\; r)\\; (\\mathrm{matPolyEquiv}\\; M)).\\mathrm{det}$$$
Lean4
theorem eval_det {R : Type*} [CommRing R] (M : Matrix n n R[X]) (r : R) :
Polynomial.eval r M.det = (Polynomial.eval (scalar n r) (matPolyEquiv M)).det :=
by
rw [Polynomial.eval, ← coe_eval₂RingHom, RingHom.map_det]
exact congr_arg det <| ext fun _ _ ↦ matPolyEquiv_eval _ _ _ _ |>.symm
