素元生成形式的 Nagata 因子性定理在 Lean 4 中的形式化

我们给出了 Nagata 因子性定理的 Lean 4 Mathlib 形式化：若 R 是诺特整环，且 S ≤ R 是一个素元生成的子幺半群，使得 S^{-1}R 是唯一分解整环，则 R 本身也是唯一分解整环。素元生成假设——S 中的每个元素都是属于 S 的素元的有限乘积——取代了一个表面更简洁但退化的素元或单位条件，而这一条件正是形式化工作所揭示的。该开发将定理同时打包为具体类型 Localization S 的版本和抽象 IsLocalization 表述。作为应用，我们形式化了两个基于 Nagata 的证明：当 R 是诺特唯一分解整环时 R[X] 也是唯一分解整环——一个通过 X 的幂的劳伦多项式局部化，另一个通过常数素元的局部化并与 Frac(R)[X] 识别。复用同一软件包，我们还得到了迭代多项式推论 R[X][Y]。据我们所知，Lean、Coq 或 Isabelle 中尚无此结果的公开形式化。