Removing the exceptional fibers

After denominator clearing, the generic-fiber argument gives coefficient vanishing away from one analytic bad factor. This file packages the pure pointwise step: fiber rigidity makes every lower-degree coefficient zero on the good locus, so multiplying by the bad factor extends the conclusion over the exceptional locus as well.

theorem LocalComplexGeometry.eventually_mul_coefficient_eq_zero_of_vanishes_on_good_fibers {n e : ℕ} (he : 0 < e) (Z : ComplexEuclidean n → Prop) (D : ComplexEuclidean n → ℂ) (q : ComplexEuclidean n → Polynomial ℂ) (b : Fin e → ComplexEuclidean n → ℂ) (hgood : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, Z z → D z ≠ 0 → q z ≠ 0 ∧ (q z).Separable ∧ (q z).natDegree = e ∧ ∀ (w : ℂ), Polynomial.eval w (q z) = 0 → Polynomial.eval w (remainderPolynomialAt b z) = 0) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, Z z → ∀ (i : Fin e), D z * b i z = 0

If a degree-< e polynomial vanishes on all roots of a separable degree-e fiber whenever D is nonzero, then every coefficient multiplied by D vanishes, including on the exceptional fibers where D = 0.

theorem LocalComplexGeometry.localSetGerm_le_germZeroLocus_mul_of_eventually {n : ℕ} (Z : LocalSetGerm n) (Zrep : ComplexEuclidean n → Prop) (D c : ComplexEuclidean n → ℂ) (hD : AnalyticAt ℂ D 0) (hc : AnalyticAt ℂ c 0) (hZ : Z = ↑Zrep) (hvanish : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, Zrep z → D z * c z = 0) : Z ≤ germZeroLocus (HolomorphicGerm.ofFunction D hD * HolomorphicGerm.ofFunction c hc)

Turn the representative-level product-vanishing conclusion into the corresponding inclusion of local set germs.