Theorems · Theorem · complex analysis
MeromorphicNFOn.div
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {x : 𝕜},
AnalyticAt 𝕜 f x → MeromorphicNFAt g x → g x ≠ 0 ∨ f x ≠ 0 → MeromorphicNFAt (f / g) x- Defined in
- Mathlib.Analysis.Meromorphic.NormalForm
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NontriviallyNormedField
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- div_eq_mul_invproof · cited by 715
- AnalyticAtstatement and proof · cited by 321
- inv_ne_zeroproof · cited by 99
- MeromorphicNFAtstatement and proof · cited by 34
- AnalyticAt.meromorphicNFAtproof · cited by 16
- AnalyticAt.invproof · cited by 13
- meromorphicNFAt_mul_iff_leftproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- Complex.meromorphicNFOn_tanhproof · cited by 1
- Complex.meromorphicNFOn_tanproof · cited by 1