Commit 2022-03-03 17:48 0da2d1d9

feat(ring_theory/polynomial/eisenstein): add mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at (#12371) We add 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. From flt-regular