Theorems · Inductive type · special functions
PeriodPair
Type
A pair of ℝ-linearly independent complex numbers.
They span the period lattice in lattice,
and are the periods of the elliptic functions we shall construct.
- Cited by
- 94 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by119
Results whose statement or proof uses this declaration.
- PeriodPair.latticestatement and proof · cited by 82
- PeriodPair.weierstrassPExceptstatement and proof · cited by 27
- PeriodPair.weierstrassPstatement and proof · cited by 22
- PeriodPair.ω₁statement and proof · cited by 22
- PeriodPair.derivWeierstrassPExceptstatement and proof · cited by 20
- PeriodPair.derivWeierstrassPstatement and proof · cited by 16
- PeriodPair.ω₂statement and proof · cited by 13
- PeriodPair.sumInvPowstatement and proof · cited by 11
- PeriodPair.ω₁_div_two_notMem_latticestatement and proof · cited by 10
- PeriodPair.weierstrassPExceptSeriesstatement and proof · cited by 8
- PeriodPair.isOpen_compl_lattice_sdiffstatement and proof · cited by 7
- PeriodPair.weierstrassPExcept_of_notMemstatement and proof · cited by 6