isIntegral

Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly

URI: https://scilib.ai/kg/mathlib#Matrix.isIntegral

English

Existence of a monic polynomial with aeval zero certifies integrality of the matrix over R.

Русский

Существование монического полинома с нулевым aeval доказывает интегральность матрицы над R.

LaTeX

$$Matrix.isIntegral$$

Lean4

theorem isIntegral : IsIntegral R M :=
  ⟨M.charpoly, ⟨charpoly_monic M, aeval_self_charpoly M⟩⟩

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

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

Разделы

Аффилиация

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