eq_zero_or_eq_zero_of_mul_eq_zero

English

If A is a NoZeroDivisors ring and f,g are analytic on a nhds of a preconnected U and f(z)·g(z)=0 for all z in U, then either f is zero on U or g is zero on U.

Русский

Если A имеет NoZeroDivisors и f,g аналитичны на nhds(U) и f(z)g(z)=0 для всех z∈U, то либо f≡0 на U, либо g≡0 на U.

LaTeX

$$$$\\forall z\\in U:\\; f(z)\\cdot g(z)=0 \\Rightarrow (\\forall z\\in U, f(z)=0) \\lor (\\forall z\\in U, g(z)=0).$$$$

Lean4

/-- If `f, g` are analytic on a neighbourhood of the preconnected open set `U`, and `f * g = 0`
on `U`, then either `f = 0` on `U` or `g = 0` on `U`. -/
theorem eq_zero_or_eq_zero_of_mul_eq_zero [NoZeroDivisors A] {f g : 𝕜 → A} (hf : AnalyticOnNhd 𝕜 f U)
    (hg : AnalyticOnNhd 𝕜 g U) (hfg : ∀ z ∈ U, f z * g z = 0) (hU : IsPreconnected U) :
    (∀ z ∈ U, f z = 0) ∨ (∀ z ∈ U, g z = 0) :=
  eq_zero_or_eq_zero_of_smul_eq_zero hf hg hfg hU

Похожие утверждения