Minimal polynomials of Eisenstein roots #
An Eisenstein polynomial over an integrally closed local domain is associated to the minimal polynomial of any of its roots in a torsion-free domain algebra.
Main results #
TauCeti.associated_minpoly_of_eisenstein_isRootidentifies the minimal polynomial up to a unit.
theorem
TauCeti.associated_minpoly_of_eisenstein_isRoot
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[IsDomain R]
[IsLocalRing R]
[IsIntegrallyClosed R]
[CommRing S]
[IsDomain S]
[Algebra R S]
[Module.IsTorsionFree R S]
(ξ : S)
(f : Polynomial R)
(hf : f.IsEisensteinAt (IsLocalRing.maximalIdeal R))
(hroot : (Polynomial.map (algebraMap R S) f).IsRoot ξ)
:
Associated (minpoly R ξ) f
The minimal polynomial of a root is associated to an Eisenstein polynomial over an integrally closed local domain.