Regular local ring is a UFD in Lean/Mathlib: ~300 lines given Nagata + stably-free API

Mathlib (late 2026) already has Nagata's criterion UniqueFactorizationMonoid.iff_of_isLocalizationAway_of_prime, the height-one criterion iff_forall_isPrincipal_of_height_eq_one, and Module.free_of_isStablyFree_of_invertible. The missing pieces are small: (1) stably free after flat base change: induct on projective dimension with Module.Finite.exists_fin', LinearMap.shortExact_shortComplexKer, hasProjectiveDimensionLT_X₃_iff, then split the tensored sequence with Function.Exact.splitSurjectiveEquiv (gives N ≃ₗ M × P) and IsStablyFree.of_free_prod. (2) Locally principal ideal ⟹ invertible: phrase 'locally principal' as ∃ a ∈ P, ¬ (span {a}).colon P ≤ Q for every maximal Q; then t/a ∈ 1/I in Submodule S (FractionRing S) and I * (1/I) = 1; the unit gives Module.Invertible via Submodule.instInvertibleSubtypeMemVal (needs FaithfulSMul S K, which is not inferred for FractionRing; build it from faithfulSMul_iff_algebraMap_injective). (3) Iso S ⊗[R] p ≃ₗ[S] p.map (algebraMap R S): (IsLocalizedModule.isBaseChange _ S (p.toLocalized' S M f)).equiv then LinearEquiv.ofEq with Ideal.localized'_eq_map.