@[implicit_reducible]

noncomputable instance dvr_normalizedGCDMonoid {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] : NormalizedGCDMonoid A

theorem primitive_exists_coeff_not_in_maxIdeal {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (g : Polynomial A) (hprim : g.IsPrimitive) : ∃ (i : ℕ), g.coeff i ∉ IsLocalRing.maximalIdeal A

theorem dvd_content_of_coeff_unit {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (h : Polynomial A) (b : A) (f : Polynomial K) (hmap : Polynomial.map (algebraMap A K) h = Polynomial.C ((algebraMap A K) b) * f) (j : ℕ) (a : A) (ha : (algebraMap A K) a = f.coeff j) (hu : IsUnit (h.primPart.coeff j)) : b ∣ h.content

theorem f_in_image_of_dvd_content {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (h : Polynomial A) (b : A) (hb : b ≠ 0) (f : Polynomial K) (hmap : Polynomial.map (algebraMap A K) h = Polynomial.C ((algebraMap A K) b) * f) (hdvd : b ∣ h.content) : ∃ (g : Polynomial A), f = Polynomial.map (algebraMap A K) g

theorem primPart_irred_of_map_irred {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (h : Polynomial A) (hh : h ≠ 0) (b : A) (hb : b ≠ 0) (f : Polynomial K) (hirr : Irreducible f) (hmap : Polynomial.map (algebraMap A K) h = Polynomial.C ((algebraMap A K) b) * f) : Irreducible h.primPart

theorem coeff_in_maxIdeal_of_not_inA {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (h : Polynomial A) (b : A) (hb : b ≠ 0) (f : Polynomial K) (hmap : Polynomial.map (algebraMap A K) h = Polynomial.C ((algebraMap A K) b) * f) (hnotinA : ¬∃ (g : Polynomial A), f = Polynomial.map (algebraMap A K) g) (j : ℕ) (a : A) (ha : (algebraMap A K) a = f.coeff j) : h.primPart.coeff j ∈ IsLocalRing.maximalIdeal A

theorem natDegree_primPart_eq {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (h : Polynomial A) (hh : h ≠ 0) (b : A) (hb : b ≠ 0) (f : Polynomial K) (hmap : Polynomial.map (algebraMap A K) h = Polynomial.C ((algebraMap A K) b) * f) : h.primPart.natDegree = f.natDegree

theorem hensel_kurschak_scaling_step' {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (f : Polynomial K) (hirr : Irreducible f) (hlead : ∃ (a : A), (algebraMap A K) a = f.leadingCoeff) (hconst : ∃ (a : A), (algebraMap A K) a = f.coeff 0) (hnotinA : ¬∃ (g : Polynomial A), f = Polynomial.map (algebraMap A K) g) : ∃ (g : Polynomial A), Irreducible g ∧ g.coeff 0 ∈ IsLocalRing.maximalIdeal A ∧ g.coeff g.natDegree ∈ IsLocalRing.maximalIdeal A ∧ ∃ (i : ℕ), g.coeff i ∉ IsLocalRing.maximalIdeal A