Mathlib Map

Theorems ยท Theorem ยท complex analysis

meromorphicNFAt_mul_iff_right

โˆ€ {๐•œ : Type u_1} [inst : NontriviallyNormedField ๐•œ] {g : ๐•œ โ†’ ๐•œ} {x : ๐•œ} {f : ๐•œ โ†’ ๐•œ},
  AnalyticAt ๐•œ g x โ†’ g x โ‰  0 โ†’ (MeromorphicNFAt (g * f) x โ†” MeromorphicNFAt f x)

If f is any function and g is analytic without zero at zโ‚€, then f is meromorphic in normal form at zโ‚€ iff g * f is meromorphic in normal form at zโ‚€.

Defined in
Mathlib.Analysis.Meromorphic.NormalForm
Cited by
0 results in Mathlib
Foundations
Depth 193 from the axioms ยท uses propext, Classical.choice, Quot.sound
Assumes
NontriviallyNormedField
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

NontriviallyNormedField ยท cited by 8742NontriviallyNormedFieldAnalyticAt ยท cited by 321AnalyticAtMeromorphicNFAt ยท cited by 34MeromorphicNFAtmeromorphicNFAt_smul_iff_right_of_analyticAt ยท cited by 3meromorphicNFAt_smul_iff_โ€ฆmeromorphicNFAt_mul_iff_rightCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.