Elementary facts about analytic function germs

The public theorem represents germs by functions modulo =ᶠ[𝓝 x]. These lemmas record the corresponding ring-theoretic unit fact without introducing a separate sheaf or stalk API into the public statement.

theorem ClassicalComplexWPT.germ_isUnit_of_eventually_ne {X : Type u_1} {l : Filter X} {g : X → ℂ} (hg : ∀ᶠ (x : X) in l, g x ≠ 0) : IsUnit ↑g

A representative which is eventually nonzero defines a unit in the function-germ ring.

theorem ClassicalComplexWPT.analytic_germ_isUnit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {g : E → ℂ} {x : E} (hg : AnalyticAt ℂ g x) (hg0 : g x ≠ 0) : IsUnit ↑g

A nonvanishing analytic germ is a ring-theoretic unit.