Mathlib Map

Theorems · Theorem · special functions

PeriodPair.meromorphic_weierstrassP

∀ (L : PeriodPair), Meromorphic L.weierstrassP
Defined in
Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Cited by
2 results in Mathlib
Foundations
Depth 294 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

PeriodPair.order_weierstrassP · cited by 0PeriodPair.order_weierstr…PeriodPair.meromorphic_derivWeierstrassP · cited by 0PeriodPair.meromorphic_de…SetLike.coe · cited by 8199SetLike.coeComplex · cited by 5565ComplexMeromorphicAt · cited by 160MeromorphicAtMeromorphic · cited by 108MeromorphicPeriodPair · cited by 94PeriodPairPeriodPair.lattice · cited by 82PeriodPair.latticeMeromorphicAt.const · cited by 36MeromorphicAt.constPeriodPair.weierstrassPExcept · cited by 27PeriodPair.weierstrassPEx…PeriodPair.weierstrassP · cited by 22PeriodPair.weierstrassPAnalyticAt.meromorphicAt · cited by 22AnalyticAt.meromorphicAtMeromorphicAt.id · cited by 18MeromorphicAt.idMeromorphicAt.fun_sub · cited by 17MeromorphicAt.fun_subMeromorphicAt.fun_add · cited by 3MeromorphicAt.fun_addPeriodPair.weierstrassPExcept_add · cited by 3PeriodPair.weierstrassPEx…PeriodPair.analyticOnNhd_weierstrassPExcept · cited by 3PeriodPair.analyticOnNhd_…PeriodPair.meromorphic_weiers…CITED BYCITES

Cites18

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

Cited by2

Results whose statement or proof uses this declaration.