noncomputable def IsDedekindDomain.HeightOneSpectrum.completionResidueMap {A : Type u_1} [CommRing A] [IsDedekindDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (𝔭 : HeightOneSpectrum A) : A →+* ↥(adicCompletionIntegers K 𝔭) ⧸ IsLocalRing.maximalIdeal ↥(adicCompletionIntegers K 𝔭)

theorem IsDedekindDomain.HeightOneSpectrum.ker_completionResidueMap {A : Type u_1} [CommRing A] [IsDedekindDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (𝔭 : HeightOneSpectrum A) : RingHom.ker 𝔭.completionResidueMap = 𝔭.asIdeal

theorem IsDedekindDomain.HeightOneSpectrum.exists_mul_sub_mem_of_not_mem {A : Type u_1} [CommRing A] [IsDedekindDomain A] (𝔭 : HeightOneSpectrum A) (b : A) (hb : b ∉ 𝔭.asIdeal) : ∃ (e : A), b * e - 1 ∈ 𝔭.asIdeal

theorem IsDedekindDomain.HeightOneSpectrum.surj_completionResidueMap {A : Type u_1} [CommRing A] [IsDedekindDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (𝔭 : HeightOneSpectrum A) : Function.Surjective ⇑𝔭.completionResidueMap