Eisenstein polynomials #
Given an ideal π
of a commutative semiring R
, we say that a polynomial f : R[X]
is
Eisenstein at π
if f.leading_coeff β π
, β n, n < f.nat_degree β f.coeff n β π
and
f.coeff 0 β π ^ 2
. In this file we gather miscellaneous results about Eisenstein polynomials.
Main definitions #
polynomial.is_eisenstein_at f π
: the property of being Eisenstein atπ
.
Main results #
polynomial.is_eisenstein_at.irreducible
: if a primitivef
satisfiesf.is_eisenstein_at π
, whereπ.is_prime
, thenf
is irreducible.mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at
: letK
be the field of fraction of an integrally closed domainR
and letL
be a separable extension ofK
, generated by an integral power basisB
such that the minimal polynomial ofB.gen
is Eisenstein atp
. Givenz : L
integral overR
, ifp ^ n β’ z β adjoin R {B.gen}
, thenz β adjoin R {B.gen}
. Together withalgebra.discr_mul_is_integral_mem_adjoin
this result often allows to compute the ring of integers ofL
.
Implementation details #
We also define a notion is_weakly_eisenstein_at
requiring only that
β n < f.nat_degree β f.coeff n β π
. This makes certain results slightly more general and it is
useful since it is sometimes better behaved (for example it is stable under polynomial.map
).
- mem : β {n : β}, n < f.nat_degree β f.coeff n β π
Given an ideal π
of a commutative semiring R
, we say that a polynomial f : R[X]
is weakly Eisenstein at π
if β n, n < f.nat_degree β f.coeff n β π
.
- leading : f.leading_coeff β π
- mem : β {n : β}, n < f.nat_degree β f.coeff n β π
- not_mem : f.coeff 0 β π ^ 2
Given an ideal π
of a commutative semiring R
, we say that a polynomial f : R[X]
is Eisenstein at π
if f.leading_coeff β π
, β n, n < f.nat_degree β f.coeff n β π
and
f.coeff 0 β π ^ 2
.
If a primitive f
satisfies f.is_eisenstein_at π
, where π.is_prime
, then f
is
irreducible.
Let K
be the field of fraction of an integrally closed domain R
and let L
be a separable
extension of K
, generated by an integral power basis B
such that the minimal polynomial of
B.gen
is Eisenstein at p
. Given z : L
integral over R
, if Q : polynomial R
is such that
aeval B.gen Q = p β’ z
, then p β£ Q.coeff 0
.
Let K
be the field of fraction of an integrally closed domain R
and let L
be a separable
extension of K
, generated by an integral power basis B
such that the minimal polynomial of
B.gen
is Eisenstein at p
. Given z : L
integral over R
, if p β’ z β adjoin R {B.gen}
, then
z β adjoin R {B.gen}
.
Let K
be the field of fraction of an integrally closed domain R
and let L
be a separable
extension of K
, generated by an integral power basis B
such that the minimal polynomial of
B.gen
is Eisenstein at p
. Given z : L
integral over R
, if p ^ n β’ z β adjoin R {B.gen}
,
then z β adjoin R {B.gen}
. Together with algebra.discr_mul_is_integral_mem_adjoin
this result
often allows to compute the ring of integers of L
.