Edge cases of classical complex Weierstrass preparation

The degree-zero case is independent of analytic division: the distinguished polynomial is 1, so the original analytic germ is the unit.

@[simp]

theorem ClassicalComplexWPT.preparedPolynomial_zero {n : ℕ} (a : Fin 0 → Base n → ℂ) (x : Ambient n) : preparedPolynomial 0 a x = 1

theorem ClassicalComplexWPT.classicalComplexWeierstrassPreparation_zero {n : ℕ} {f : Ambient n → ℂ} (hf : AnalyticAt ℂ f 0) (horder : ExactOrderInLastVariable f 0) : ∃ (a : Fin 0 → Base n → ℂ) (u : Ambient n → ℂ), IsWeierstrassPreparation f 0 a u ∧ ∀ (a' : Fin 0 → Base n → ℂ) (u' : Ambient n → ℂ), IsWeierstrassPreparation f 0 a' u' → (∀ (i : Fin 0), a i =ᶠ[nhds 0] a' i) ∧ u =ᶠ[nhds 0] u'

Degree-zero preparation, including uniqueness of the empty coefficient family and the unit.

theorem ClassicalComplexWPT.classicalComplexWeierstrassPreparation_noBase {d : ℕ} {f : Ambient 0 → ℂ} (hf : AnalyticAt ℂ f 0) (horder : ExactOrderInLastVariable f d) : ∃ (a : Fin d → Base 0 → ℂ) (u : Ambient 0 → ℂ), IsWeierstrassPreparation f d a u ∧ ∀ (a' : Fin d → Base 0 → ℂ) (u' : Ambient 0 → ℂ), IsWeierstrassPreparation f d a' u' → (∀ (i : Fin d), a i =ᶠ[nhds 0] a' i) ∧ u =ᶠ[nhds 0] u'

When there are no base variables, preparation is precisely the univariate exact-order factorization. This proves the full public existence-and- uniqueness conclusion for every degree d when n = 0.