The zero-dimensional prime case

The analytic Nullstellensatz induction starts in complex dimension zero. The germ ring there is canonically ℂ, so its only prime ideal is zero; the zero ideal has the full neighborhood as its zero-set germ.

theorem LocalComplexGeometry.holomorphicGerm_zero_prime_eq_bot (P : Ideal ↥(HolomorphicGerm 0)) (hP : P.IsPrime) : P = ⊥

Every prime ideal of the zero-dimensional holomorphic germ ring is zero.

theorem LocalComplexGeometry.primeZeroSetProperty_zero : PrimeZeroSetProperty 0

The prime zero-set theorem in complex dimension zero.