minpoly_toLin'

Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly

URI: https://scilib.ai/kg/mathlib#Matrix.minpoly_toLin'

English

Any square matrix over a field is integral; its minimal polynomial lies in the ring.

Русский

Любая квадратная матрица над полем интегральна; её минимальный полином лежит в кольце.

LaTeX

$$Matrix.isIntegral R M$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru