Degree bounds for integral elements: over an integrally closed base ring, the minimal polynomial of an integral element has degree at most the degree of the fraction-field extension.

theorem CCDN.integral_minpoly_natDegree_le_fraction_finrank (R : Type u_1) (A : Type u_2) (F : Type u_3) (E : Type u_4) [CommRing R] [IsDomain R] [IsIntegrallyClosed R] [CommRing A] [IsDomain A] [Field F] [Field E] [Algebra R A] [Algebra R F] [IsFractionRing R F] [Algebra R E] [Algebra A E] [Algebra F E] [IsScalarTower R A E] [IsScalarTower R F E] [FiniteDimensional F E] (a : A) (ha : IsIntegral R a) : (minpoly R a).natDegree ≤ Module.finrank F E

Let R be an integrally closed domain with fraction field F, and let E be a finite extension of F receiving compatible maps from R, A and F. The minimal polynomial over R of an integral element a of the domain A has degree at most [E : F].