feat: progress towards Rat.AdeleRing.zero_discrete

FLT/Mathlib/NumberTheory/NumberField/Basic.lean

@@ -4,4 +4,5 @@ open scoped NumberField
 
 theorem Rat.ringOfIntegersEquiv_eq_algebraMap (z : 𝓞 ℚ) :
     (Rat.ringOfIntegersEquiv z : ℚ) = algebraMap (𝓞 ℚ) ℚ z := by
-  sorry -- #307
+  obtain ⟨z, rfl⟩ := Rat.ringOfIntegersEquiv.symm.surjective z
+  simp

FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

@@ -0,0 +1,37 @@
+import Mathlib.RingTheory.DedekindDomain.AdicValuation
+
+open IsDedekindDomain
+
+-- mathlib PR #20523
+namespace IsDedekindDomain.HeightOneSpectrum
+
+variable (R K : Type*) [CommRing R] [Field K] [IsDedekindDomain R] [Algebra R K]
+    [IsFractionRing R K] in
+theorem mem_integers_of_valuation_le_one (x : K)
+    (h : ∀ v : HeightOneSpectrum R, v.valuation x ≤ 1) : x ∈ (algebraMap R K).range := by
+  obtain ⟨⟨n, d, hd⟩, hx⟩ := IsLocalization.surj (nonZeroDivisors R) x
+  obtain rfl : x = IsLocalization.mk' K n ⟨d, hd⟩ := IsLocalization.eq_mk'_iff_mul_eq.mpr hx
+  have hd0 := nonZeroDivisors.ne_zero hd
+  obtain rfl | hn0 := eq_or_ne n 0
+  · simp
+  suffices Ideal.span {d} ∣ (Ideal.span {n} : Ideal R) by
+    obtain ⟨z, rfl⟩ := Ideal.span_singleton_le_span_singleton.1 (Ideal.le_of_dvd this)
+    use z
+    rw [map_mul, mul_comm,mul_eq_mul_left_iff] at hx
+    cases' hx with h h
+    · exact h.symm
+    · simp [hd0] at h
+  classical
+  have ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥ := fun {r} ↦ mt Ideal.span_singleton_eq_bot.mp
+  rw [← Associates.mk_le_mk_iff_dvd, ← Associates.factors_le, Associates.factors_mk _ (ine hn0),
+    Associates.factors_mk _ (ine hd0), WithTop.coe_le_coe, Multiset.le_iff_count]
+  rintro ⟨v, hv⟩
+  obtain ⟨v, rfl⟩ := Associates.mk_surjective v
+  have hv' := hv
+  rw [Associates.irreducible_mk, irreducible_iff_prime] at hv
+  specialize h ⟨v, Ideal.isPrime_of_prime hv, hv.ne_zero⟩
+  simp_rw [valuation_of_mk', intValuation, ← Valuation.toFun_eq_coe,
+    intValuationDef_if_neg _ hn0, intValuationDef_if_neg _ hd0, ← WithZero.coe_div,
+    ← WithZero.coe_one, WithZero.coe_le_coe, Associates.factors_mk _ (ine hn0),
+    Associates.factors_mk _ (ine hd0), Associates.count_some hv'] at h
+  simpa using h

FLT/NumberField/AdeleRing.lean

@@ -1,4 +1,6 @@
 import Mathlib
+import FLT.Mathlib.NumberTheory.NumberField.Basic
+import FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation
 
 universe u
 
@@ -49,17 +51,15 @@ theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
       change ‖(x : ℂ)‖ < 1 at h1
       simp at h1
       have intx: ∃ (y:ℤ), y = x
-      · clear h1 -- not needed
-        -- mathematically this is trivial:
-        -- h2 says that no prime divides the denominator of x
-        -- so x is an integer
-        -- and the goal is that there exists an integer `y` such that `y = x`.
-        suffices ∀ p : ℕ, p.Prime → ¬(p ∣ x.den) by
-          use x.num
-          rw [← den_eq_one_iff]
-          contrapose! this
-          exact ⟨x.den.minFac, Nat.minFac_prime this, Nat.minFac_dvd _⟩
-        sorry -- issue #254
+      · obtain ⟨z, hz⟩ := IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one
+            (𝓞 ℚ) ℚ x <| fun v ↦ by
+          specialize h2 v
+          letI : UniformSpace ℚ := v.adicValued.toUniformSpace
+          rw [IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers] at h2
+          rwa [← IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation']
+        use Rat.ringOfIntegersEquiv z
+        rw [← hz]
+        apply Rat.ringOfIntegersEquiv_eq_algebraMap
       obtain ⟨y, rfl⟩ := intx
       simp only [abs_lt] at h1
       norm_cast at h1 ⊢