minpoly_toMatrix — Mathlib

English

Let b be a basis of N and f a linear map N → N. The minimal polynomial of the matrix of f with respect to the basis b equals the minimal polynomial of f.

Русский

Пусть b – базис пространства N и f – линейное отображение N → N. Минимальный полином матрицы представления f в базисе b совпадает с минимальным полином самого f.

LaTeX

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

Lean4

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

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