Documentation

LeanPool.LocalComplexGeometry

Foundational local complex-analytic geometry #

Source: url:https://github.com/BochaoKong/nullstellensatz Authors: BochaoKong Status: verified Main declarations: LocalComplexGeometry.localAnalyticNullstellensatz Tags: complex-analysis, analytic-geometry, nullstellensatz, weierstrass-preparation MSC: 32A05, 32A10, 32B05, 32C25, 13E05

Local complex-analytic geometry #

This root module exposes the seven kernel-checked headline results, the public examples and corollaries, and their shared local complex-analytic geometry infrastructure.