Eisenstein polynomials over discrete valuation rings

The Eisenstein condition over a discrete valuation ring makes the constant coefficient a uniformizer. Conversely, X ^ n minus a uniformizer is Eisenstein for positive n.

Main results

• Polynomial.IsEisensteinAt.irreducible_coeff_zero identifies the constant coefficient as an irreducible element.
• TauCeti.isEisensteinAt_X_pow_sub_C_of_irreducible gives Eisenstein polynomials from uniformizers.

theorem Polynomial.IsEisensteinAt.irreducible_coeff_zero {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {f : Polynomial R} (hf : f.IsEisensteinAt (IsLocalRing.maximalIdeal R)) (hdeg : 0 < f.natDegree) : Irreducible (f.coeff 0)

The constant coefficient of an Eisenstein polynomial of positive degree over a discrete valuation ring is irreducible.

theorem TauCeti.isEisensteinAt_X_pow_sub_C_of_irreducible {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {ϖ : R} (hϖ : Irreducible ϖ) {n : ℕ} (hn : 0 < n) : (Polynomial.X ^ n - Polynomial.C ϖ).IsEisensteinAt (IsLocalRing.maximalIdeal R)

Over a discrete valuation ring, X ^ n minus a uniformizer is Eisenstein for positive n.