Cancellation on a prime analytic zero set

The generic-fiber proof repeatedly clears a denominator D which is not in the contracted prime. If D * c vanishes on that prime's local zero set, the lower-dimensional prime theorem puts the product in the prime, and primality cancels D.

theorem LocalComplexGeometry.mem_prime_of_mul_mem_of_not_mem {n : ℕ} {P : Ideal ↥(HolomorphicGerm n)} (hP : P.IsPrime) {D c : ↥(HolomorphicGerm n)} (hD : D ∉ P) (hDc : D * c ∈ P) : c ∈ P

Cancel a nonmember from a product in a prime ideal.

theorem LocalComplexGeometry.mem_prime_of_mul_vanishes_on_zeroSet {n : ℕ} (hprime : PrimeZeroSetProperty n) (P : Ideal ↥(HolomorphicGerm n)) (hP : P.IsPrime) {D c : ↥(HolomorphicGerm n)} (hD : D ∉ P) (hvanish : idealZeroSetGerm P ≤ germZeroLocus (D * c)) : c ∈ P

Prime zero-set cancellation in the exact form used after denominator clearing.

theorem LocalComplexGeometry.finset_prod_not_mem_prime {R : Type u_1} [CommRing R] {P : Ideal R} (hP : P.IsPrime) {ι : Type u_2} (S : Finset ι) (f : ι → R) (hf : ∀ i ∈ S, f i ∉ P) : ∏ i ∈ S, f i ∉ P

A finite product of elements outside a prime remains outside the prime.