Theorems · Theorem · complex analysis

Meromorphic.fun_prod

∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_5} {s : Finset ι} {F : ι → 𝕜 → 𝕜'},
  (∀ σ ∈ s, Meromorphic (F σ)) → Meromorphic fun a => ∏ c ∈ s, F c a

Eta-expanded form of Meromorphic.prod

Defined in: Mathlib.Analysis.Meromorphic.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NontriviallyNormedField NontriviallyNormedField NormedAlgebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites7

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

Finsetstatement and proof · cited by 13,712
NontriviallyNormedFieldstatement and proof · cited by 8,742
Finset.prodstatement · cited by 2,356
NormedAlgebrastatement and proof · cited by 1,165
Meromorphicstatement and proof · cited by 108
Finset.prod_fnproof · cited by 9
Meromorphic.prodproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.