Rückert's basis theorem

The induction is the classical analytic proof. A nonzero element of an ideal is made regular in the last variable, Weierstrass preparation replaces it by an associated distinguished polynomial, and Weierstrass division maps the ideal into a finite lower-dimensional remainder module.

theorem LocalComplexGeometry.holomorphicGerm_isNoetherian_core (n : ℕ) : IsNoetherianRing ↥(HolomorphicGerm n)

Rückert's basis theorem. The local ring of holomorphic germs at the origin of every finite-dimensional complex affine space is Noetherian.

instance LocalComplexGeometry.holomorphicGerm_instIsNoetherianRing (n : ℕ) : IsNoetherianRing ↥(HolomorphicGerm n)

The Noetherian structure supplied by Rückert's theorem.