Mathlib Map

Theorems · Theorem · complex analysis

meromorphicOrderAt_mul

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f g : 𝕜 → 𝕜'},
  MeromorphicAt f x → MeromorphicAt g x → meromorphicOrderAt (f * g) x = meromorphicOrderAt f x + meromorphicOrderAt g x

The order is additive when multiplying meromorphic functions.

Defined in
Mathlib.Analysis.Meromorphic.Order
Cited by
4 results in Mathlib
Foundations
Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NontriviallyNormedFieldNontriviallyNormedFieldNormedAlgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

meromorphicOrderAt_prod · cited by 3meromorphicOrderAt_prodmeromorphicOrderAt_div · cited by 2meromorphicOrderAt_divmeromorphicOrderAt_pow · cited by 2meromorphicOrderAt_powfun_meromorphicOrderAt_mul · cited by 1fun_meromorphicOrderAt_mulNontriviallyNormedField · cited by 8742NontriviallyNormedFieldWithTop · cited by 3754WithTopNormedAlgebra · cited by 1165NormedAlgebrameromorphicOrderAt · cited by 180meromorphicOrderAtMeromorphicAt · cited by 160MeromorphicAtmeromorphicOrderAt_smul · cited by 10meromorphicOrderAt_smulmeromorphicOrderAt_mulCITED BYCITES

Cites6

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

Cited by4

Results whose statement or proof uses this declaration.