Eisenstein polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. In this file we gather more miscellaneous results about Eisenstein polynomials

Main results #

mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at: 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.

source

theorem cyclotomic_comp_X_add_one_is_eisenstein_at (p : ℕ) [hp : fact (nat.prime p)] :

((polynomial.cyclotomic p ℤ).comp (polynomial.X + 1)).is_eisenstein_at (submodule.span ℤ {↑p})

source

theorem cyclotomic_prime_pow_comp_X_add_one_is_eisenstein_at (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

((polynomial.cyclotomic (p ^ (n + 1)) ℤ).comp (polynomial.X + 1)).is_eisenstein_at (submodule.span ℤ {↑p})

source

theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_is_eiseinstein_at {R : Type u} {K : Type v} {L : Type z} {p : R} [comm_ring R] [field K] [field L] [algebra K L] [algebra R L] [algebra R K] [is_scalar_tower R K L] [is_separable K L] [is_domain R] [is_fraction_ring R K] [is_integrally_closed R] {B : power_basis K L} (hp : prime p) (hBint : is_integral R B.gen) {z : L} {Q : polynomial R} (hQ : ⇑(polynomial.aeval B.gen) Q = p • z) (hzint : is_integral R z) (hei : (minpoly R B.gen).is_eisenstein_at (submodule.span R {p})) :

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 Q : R[X] is such that aeval B.gen Q = p • z, then p ∣ Q.coeff 0.

source

theorem mem_adjoin_of_dvd_coeff_of_dvd_aeval {A : Type u_1} {B : Type u_2} [comm_semiring A] [comm_ring B] [algebra A B] [no_zero_smul_divisors A B] {Q : polynomial A} {p : A} {x z : B} (hp : p ≠ 0) (hQ : ∀ (i : ℕ), i ∈ finset.range (Q.nat_degree + 1) → p ∣ Q.coeff i) (hz : ⇑(polynomial.aeval x) Q = p • z) :

z ∈ algebra.adjoin A {x}

source

theorem mem_adjoin_of_smul_prime_smul_of_minpoly_is_eiseinstein_at {R : Type u} {K : Type v} {L : Type z} {p : R} [comm_ring R] [field K] [field L] [algebra K L] [algebra R L] [algebra R K] [is_scalar_tower R K L] [is_separable K L] [is_domain R] [is_fraction_ring R K] [is_integrally_closed R] {B : power_basis K L} (hp : prime p) (hBint : is_integral R B.gen) {z : L} (hzint : is_integral R z) (hz : p • z ∈ algebra.adjoin R {B.gen}) (hei : (minpoly R B.gen).is_eisenstein_at (submodule.span R {p})) :

z ∈ algebra.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 • z ∈ adjoin R {B.gen}, then z ∈ adjoin R {B.gen}.

source

theorem mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at {R : Type u} {K : Type v} {L : Type z} {p : R} [comm_ring R] [field K] [field L] [algebra K L] [algebra R L] [algebra R K] [is_scalar_tower R K L] [is_separable K L] [is_domain R] [is_fraction_ring R K] [is_integrally_closed R] {B : power_basis K L} (hp : prime p) (hBint : is_integral R B.gen) {n : ℕ} {z : L} (hzint : is_integral R z) (hz : p ^ n • z ∈ algebra.adjoin R {B.gen}) (hei : (minpoly R B.gen).is_eisenstein_at (submodule.span R {p})) :

z ∈ algebra.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.