analyticOrderAt_mul — Mathlib

English

If f and g are analytic at z0, then the analytic order of their product equals the sum of their orders.

Русский

Если f и g аналитичны в z0, то порядок их произведения равен сумме порядков.

LaTeX

$$$analyticOrderAt\, f\, z_0 \;\text{и}\; analyticOrderAt\, g\, z_0\;\Rightarrow\; analyticOrderAt\,(f\cdot g)\, z_0 = analyticOrderAt\, f\, z_0 + analyticOrderAt\, g\, z_0$$$

Lean4

/-- The order is additive when multiplying analytic functions. -/
theorem analyticOrderAt_mul (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) :
    analyticOrderAt (f * g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀ :=
  analyticOrderAt_smul hf hg

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