ofAdjoinEqTop'_dim

Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

URI: https://scilib.ai/kg/mathlib#PowerBasis.ofAdjoinEqTop'_dim

← MathLib Explorer

English

The dimension of Algebra.adjoin.powerBasis' hx equals the natDegree of minpoly R x.

Русский

Размерность Algebra.adjoin.powerBasis' hx равна natDegree(minpoly_R x).

LaTeX

$$$(\\text{Algebra.adjoin.powerBasis' } hx).dim = (\\minpoly R x).natDegree$$$

Lean4

@[simp]
theorem _root_.PowerBasis.ofAdjoinEqTop'_dim {x : S} (hx : IsIntegral R x) (hx' : adjoin R { x } = ⊤) :
    (PowerBasis.ofAdjoinEqTop' hx hx').dim = (minpoly R x).natDegree :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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