Lean/Mathlib: Noetherian from Noetherian localizations + finite character, via R/(x)

Mathlib (v4.35-era) has IsNoetherianRing.of_isLocalization_maximal only for semilocal rings ([Finite (MaximalSpectrum R)], RingTheory/LocalProperties/Semilocal.lean). The finite-character version needs no new machinery: R is Noetherian if every R_P (P maximal) is Noetherian and each x ≠ 0 lies in finitely many maximal ideals. For an ideal J ≠ ⊥ pick 0 ≠ x ∈ J (Submodule.exists_mem_ne_zero_of_ne_bot). R ⧸ (x) is semilocal: inject MaximalSpectrum (R ⧸ K) into the finite set with Ideal.comap_isMaximal_of_surjective and Ideal.comap_injective_of_surjective. Its localizations are images of R_P: isNoetherianRing_of_surjective with Localization.localRingHom (Q.comap f) Q f rfl and RingHom.surjectiveOnStalks_of_surjective hf Q inferInstance. Then lift generators of J.map f with Ideal.mem_map_iff_of_surjective + Finset.subset_set_image_iff, and Ideal.comap_map_of_surjective + Ideal.mk_ker give J = span t ⊔ (x). Corollary: an almost Dedekind domain of finite character is Dedekind, via isDedekindDomain_iff_isDiscreteValuationRing_atPrime. Gotchas: in a module file IsLocalization.isNoetherianRing was 'Unknown constant' until I explicitly imported Mathlib.RingTheory.Localization.Submodule (transitive imports were not enough). The 'nonzero x in finitely many maximal ideals' converse needs only Ring.DimensionLEOne + Noetherian, no IsDomain: the maximal ideals are in (Ideal.span {x}).minimalPrimes, finite by Ideal.finite_minimalPrimes_of_isNoetherianRing.