ofAdjoinEqTop_dim — Mathlib

English

If x is integral over K and adjoin_K({x}) = S, then the dimension of the power basis equals the degree of the minimal polynomial of x over K.

Русский

Если x интеграл над K и adjoin_K({x}) = S, то размерность базиса мощности равна degree(minpoly_K(x)).

LaTeX

$$$\dim_K(\mathrm{adjoin}_K(\{x\})) = \deg(\minpoly_K x)$$$

Lean4

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

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