powerBasis'_dim — Mathlib

English

For hx integral, the dimension of the transported power basis equals the degree (natDegree) of the minimal polynomial of x over R.

Русский

Пусть hx интегрально над R. Размерность перенесенного базиса мощности равна степени минимального полинома x над R.

LaTeX

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

Lean4

@[simp]
theorem _root_.Algebra.adjoin.powerBasis'_dim (hx : IsIntegral R x) :
    (Algebra.adjoin.powerBasis' hx).dim = (minpoly R x).natDegree :=
  rfl

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