minpoly_toLin — Mathlib

English

The minimal polynomial of a matrix equals the minimal polynomial of the corresponding linear operator under a basis isomorphism.

Русский

Минимальный полином матрицы равен минимальному полиному линейного оператора при базисном изоморфизме.

LaTeX

$$Matrix.minpoly_toLin M$$

Lean4

@[simp]
theorem minpoly_toLin (b : Basis n R N) (M : Matrix n n R) : minpoly R (toLin b b M) = minpoly R M :=
  minpoly.algEquiv_eq (toLinAlgEquiv b : Matrix n n R ≃ₐ[R] _) M

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