degree_dvd — Mathlib

English

If x ∈ L is integral over K, then the natDegree of minpoly K x divides the finite dimension finrank K L.

Русский

Если x интеграл над K, то natDegree(minpoly K x) делитfinrank_K L.

LaTeX

$$$(\operatorname{natDegree}(\minpoly K x)) \mid \operatorname{finrank}_K L$$$

Lean4

/-- If `x : L` is an integral element in a field extension `L` over `K`, then the degree of the
  minimal polynomial of `x` over `K` divides `[L : K]`. -/
theorem _root_.minpoly.degree_dvd {x : L} (hx : IsIntegral K x) : (minpoly K x).natDegree ∣ finrank K L :=
  by
  rw [dvd_iff_exists_eq_mul_left, ← IntermediateField.adjoin.finrank hx]
  use finrank K⟮x⟯ L
  rw [mul_comm, finrank_mul_finrank]
    -- TODO: generalize to `Sort`

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