English
Let x lie in an extension L of K and be integral over K. Then the degree of the minimal polynomial of x over K equals the dimension of the K-algebra K⟮x⟯ over K; equivalently [K(x):K] = deg(minpoly_K x).
Русский
Пусть x лежит в расширении L над K и интегрирован над K. Тогда степень минимального полинома x над K равна размерности пространства K⟮x⟯ над K; то есть [K(x):K] = deg(minpoly_K x).
LaTeX
$$$\operatorname{finrank}_K\bigl(K\langle x\rangle\bigr) = \operatorname{natDegree}\bigl(\minpoly K x\bigr)$$$
Lean4
/-- If `x` is an algebraic element of field `K`, then its minimal polynomial has degree
`[K(x) : K]`. -/
@[stacks 09GN]
theorem finrank {x : L} (hx : IsIntegral K x) : Module.finrank K K⟮x⟯ = (minpoly K x).natDegree :=
by
rw [PowerBasis.finrank (adjoin.powerBasis hx :)]
rfl
