Theorems · Theorem · special functions
PeriodPair.weierstrassPExcept_add
∀ (L : PeriodPair) (l₀ : ↥L.lattice) (z : ℂ), L.weierstrassPExcept (↑l₀) z + (1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2) = L.weierstrassP z
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 211 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpaceproof · cited by 24,529
- AddCommMonoidproof · cited by 12,281
- Submodulestatement · cited by 7,192
- Complexstatement and proof · cited by 5,565
- add_zeroproof · cited by 2,707
- zero_addproof · cited by 2,366
- SummationFilter.unconditionalproof · cited by 2,068
- tsumproof · cited by 1,148
- one_divproof · cited by 624
- Function.supportproof · cited by 610
- SummationFilterproof · cited by 607
- Set.Finite.subsetproof · cited by 285
Cited by3
Results whose statement or proof uses this declaration.
- PeriodPair.meromorphic_weierstrassPproof · cited by 2
- PeriodPair.not_continuousAt_weierstrassPproof · cited by 1
- PeriodPair.weierstrassPExcept_defproof · cited by 0