theorem minpoly_natDegree_le_finrank {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (α : L) [FiniteDimensional K L] : (minpoly K α).natDegree ≤ Module.finrank K L

The natDegree of the minimal polynomial of any element of a finite extension is bounded by the degree of the extension.

theorem minpoly_degree_le_finrank {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (α : L) [FiniteDimensional K L] : (minpoly K α).degree ≤ ↑(Module.finrank K L)

The polynomial degree of the minimal polynomial of any element of a finite extension is bounded by the degree of the extension.

theorem minpoly_natDegree_dvd_finrank {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (α : L) [FiniteDimensional K L] : (minpoly K α).natDegree ∣ Module.finrank K L

The degree of the minimal polynomial of any element of a finite extension divides the degree of the extension.