{"id":"palomar/PALOMAR-2026-08-29-000010","url":"https://github.com/BochaoKong/classical-complex-wpt/tree/b4a7273fe5c9752753c52e10494097569089642d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-29-000010-v1.json","repo":"https://github.com/BochaoKong/classical-complex-wpt","tags":["math.CV","msc:32A05","msc:32A10","msc:32B05","complex-analysis","several-complex-variables","lean-formalization","weierstrass-preparation"],"score":0,"title":"BochaoKong/classical-complex-wpt","trust":"high","domain":"math.CV","source":"palomar","authors":["BochaoKong"],"reviews":0,"subject":"math.CV","summary":"A Mathlib-only Lean 4 formalization of the classical complex-analytic Weierstrass preparation theorem at the origin. For every number of base variables and every preparation degree, including the zero-dimensional and degree-zero cases, it constructs the distinguished monic polynomial and nonvanishing analytic unit and proves uniqueness of all factors as germs.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-29","reactions":{},"formalized":true}