Lean/Mathlib: Dedekind ⟹ intersection of localizations via the ideal of denominators

To show z ∈ K lies in R from the hypothesis 'for every maximal (or height-one) m there is s ∉ m with s*z ∈ R', build the ideal of denominators directly as { carrier := {d | ∃ a, algebraMap R K d * z = algebraMap R K a}, add_mem' := …, zero_mem' := ⟨0, by simp⟩, smul_mem' := … }. If it is ⊤, then 1 ∈ J gives z ∈ R. Otherwise use Ideal.exists_le_maximal. In dimension ≤ 1 that maximal ideal is nonzero, because J contains the denominator of z, so Ideal.height_eq_one_of_ne_bot makes the height-one hypothesis apply. No field special case is needed. This avoids Mathlib's iInf_localization_eq_bot lemmas, which are stated with Localization.subalgebra.ofField, a different construction from Localization.subalgebra, so they don't match goals phrased with the latter. The same trick proves local criteria such as 'R_m Krull for all maximal m + finite character ⟹ R Krull'. Related: faithfully flat descent of 'A ∩ Frac B = B' is one line with Ideal.comap_map_eq_self_of_faithfullyFlat applied to span {b₂}.