@[reducible, inline]

abbrev Polynomial.IsEisenstein {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (f : Polynomial A) : Prop

theorem Polynomial.IsEisenstein.irreducible_in_ring {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {f : Polynomial A} (heis : f.IsEisenstein) (hf : f.Monic) (hdeg : 0 < f.natDegree) : Irreducible f

theorem Polynomial.IsEisenstein.irreducible_map_fractionField {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {f : Polynomial A} (heis : f.IsEisenstein) (hf : f.Monic) (hdeg : 0 < f.natDegree) {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] : Irreducible (map (algebraMap A K) f)

theorem coeff0_image_mem_span_root {A : Type u_2} [CommRing A] (f : Polynomial A) : (algebraMap A (AdjoinRoot f)) (f.coeff 0) ∈ Ideal.span {AdjoinRoot.root f}

theorem maximalIdeal_eq_span_coeff0 {A : Type u_2} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (f : Polynomial A) (heis : f.IsEisensteinAt (IsLocalRing.maximalIdeal A)) (hdeg : 0 < f.natDegree) : IsLocalRing.maximalIdeal A = Ideal.span {f.coeff 0}

theorem map_maxIdeal_le_span_root {A : Type u_2} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (f : Polynomial A) (heis : f.IsEisensteinAt (IsLocalRing.maximalIdeal A)) (hdeg : 0 < f.natDegree) : Ideal.map (algebraMap A (AdjoinRoot f)) (IsLocalRing.maximalIdeal A) ≤ Ideal.span {AdjoinRoot.root f}

theorem adjoinRoot_root_ne_zero {A : Type u_2} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (f : Polynomial A) (heis : f.IsEisensteinAt (IsLocalRing.maximalIdeal A)) (hf : f.Monic) (hdeg : 0 < f.natDegree) : AdjoinRoot.root f ≠ 0

theorem adjoinRoot_eisenstein_isDVR {A : Type u_2} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (f : Polynomial A) (heis : f.IsEisensteinAt (IsLocalRing.maximalIdeal A)) (hf : f.Monic) (hdeg : 0 < f.natDegree) [h_local : IsLocalRing (AdjoinRoot f)] (h_maxeq_cor : IsLocalRing.maximalIdeal (AdjoinRoot f) = Ideal.map (algebraMap A (AdjoinRoot f)) (IsLocalRing.maximalIdeal A) ⊔ Ideal.span {AdjoinRoot.root f}) : IsDiscreteValuationRing (AdjoinRoot f)

theorem residue_aeval_eq_residue_const {A : Type u_2} [CommRing A] {B : Type u_3} [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] (π : B) (hπ_mem : π ∈ IsLocalRing.maximalIdeal B) (p : Polynomial A) : (IsLocalRing.residue B) ((Polynomial.aeval π) p) = (IsLocalRing.residue B) ((algebraMap A B) (p.coeff 0))

theorem residueField_map_surj_of_adjoin_uniformizer {A : Type u_2} [CommRing A] {B : Type u_3} [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalRing A] [IsLocalHom (algebraMap A B)] (π : B) (hπ : Irreducible π) (hadj : A[π] = ⊤) : Function.Surjective ⇑(IsLocalRing.ResidueField.map (algebraMap A B))

theorem finrank_eq_one_of_algebraMap_surjective {k : Type u_4} {l : Type u_5} [Field k] [Field l] [Algebra k l] (hsurj : Function.Surjective ⇑(algebraMap k l)) : Module.finrank k l = 1

theorem eisenstein_implies_totally_ramified (A : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_4) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_5) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (π : B) (hπ : Irreducible π) (hadj : A[π] = ⊤) (_heis : (minpoly A π).IsEisensteinAt (IsLocalRing.maximalIdeal A)) : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = Module.finrank K L

theorem uniformizer_powers_span_mod_maximal (A : Type u_6) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_7) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_8) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_9) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (π : B) (hπ : Irreducible π) (htotram : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = Module.finrank K L) : ⊤ ≤ Subalgebra.toSubmodule A[π] ⊔ IsLocalRing.maximalIdeal A • ⊤

theorem totally_ramified_adjoin_uniformizer (A : Type u_6) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_7) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_8) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_9) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (π : B) (hπ : Irreducible π) (htotram : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = Module.finrank K L) : A[π] = ⊤

theorem totally_ramified_minpoly_coeff_mem (A : Type u_6) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_7) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_8) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_9) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (π : B) (_hπ : Irreducible π) (_htotram : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = Module.finrank K L) {n : ℕ} (_hn : n < (minpoly A π).natDegree) : (minpoly A π).coeff n ∈ IsLocalRing.maximalIdeal A

theorem totally_ramified_coeff0_image_not_in_pow_succ (A : Type u_6) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_7) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_8) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_9) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (π : B) (_hπ : Irreducible π) (_htotram : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = Module.finrank K L) : (algebraMap A B) ((minpoly A π).coeff 0) ∉ IsLocalRing.maximalIdeal B ^ (Module.finrank K L + 1)

theorem totally_ramified_minpoly_coeff0_notMem_sq (A : Type u_6) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_7) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_8) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_9) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (π : B) (_hπ : Irreducible π) (_htotram : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = Module.finrank K L) : (minpoly A π).coeff 0 ∉ IsLocalRing.maximalIdeal A ^ 2

theorem totally_ramified_minpoly_eisenstein (A : Type u_6) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_7) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_8) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_9) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (π : B) (hπ : Irreducible π) (htotram : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = Module.finrank K L) : (minpoly A π).IsEisensteinAt (IsLocalRing.maximalIdeal A)

theorem totally_ramified_implies_eisenstein_and_adjoin (A : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_4) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_5) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (π : B) (hπ : Irreducible π) (htotram : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = Module.finrank K L) : A[π] = ⊤ ∧ (minpoly A π).IsEisensteinAt (IsLocalRing.maximalIdeal A)

theorem totally_ramified_iff_eisenstein_adjoin (A : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_4) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_5) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (π : B) (hπ : Irreducible π) : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = Module.finrank K L ↔ A[π] = ⊤ ∧ (minpoly A π).IsEisensteinAt (IsLocalRing.maximalIdeal A)