minpoly_toMatrix' — Mathlib

English

For a linear map f: (n → R) →ₗ[R] n → R over a ring R, its minimal polynomial is preserved by passing to its matrix representation; i.e., minpoly R (toMatrix' f) = minpoly R f.

Русский

Для линейного отображения f: (n → R) →ₗ[R] n → R над кольцом R минимальный полином сохраняется при переходе к его матричному представлению; то есть minpoly R (toMatrix' f) = minpoly R f.

LaTeX

$$$\\minpoly R (toMatrix' f) = \\minpoly R f$$$

Lean4

@[simp]
theorem minpoly_toMatrix' (f : (n → R) →ₗ[R] n → R) : minpoly R (toMatrix' f) = minpoly R f :=
  minpoly.algEquiv_eq (toMatrixAlgEquiv' : _ ≃ₐ[R] Matrix n n R) f

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