Theorems · Theorem · complex analysis
MeromorphicAt.id
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), MeromorphicAt id x- Defined in
- Mathlib.Analysis.Meromorphic.Basic
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 187 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.
Cites4
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
- MeromorphicAtstatement · cited by 160
- analyticAt_idproof · cited by 39
- AnalyticAt.meromorphicAtproof · cited by 22
Cited by18
Results whose statement or proof uses this declaration.
- AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNEproof · cited by 11
- MeromorphicAt.derivproof · cited by 6
- Complex.meromorphic_canonicalFactorproof · cited by 5
- AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNEproof · cited by 4
- Complex.meromorphicOrderAt_canonicalFactorproof · cited by 3
- meromorphicNFAt_iff_analyticAt_orproof · cited by 3
- meromorphicOrderAt_zpow_id_sub_constproof · cited by 3
- meromorphicOrderAt_addproof · cited by 2
- circleIntegrable_log_norm_sub_constproof · cited by 2
- MeromorphicOn.idproof · cited by 2
- PeriodPair.meromorphic_weierstrassPproof · cited by 2