Commit 2025-11-25 09:29 4322ca42

View on Github →

feat(Analysis): Weierstrass ℘ functions (#31294)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean

added theorem PeriodPair.basis_one

added theorem PeriodPair.basis_zero

added theorem PeriodPair.differentiableOn_℘

added theorem PeriodPair.differentiableOn_℘Except

added theorem PeriodPair.finrank_lattice

added theorem PeriodPair.hasSumLocallyUniformly_aux

added theorem PeriodPair.hasSumLocallyUniformly_℘

added theorem PeriodPair.hasSumLocallyUniformly_℘Except

added theorem PeriodPair.hasSum_℘

added theorem PeriodPair.hasSum_℘Except

added theorem PeriodPair.isClosed_lattice

added theorem PeriodPair.isClosed_of_subset_lattice

added def PeriodPair.lattice

added def PeriodPair.latticeBasis

added theorem PeriodPair.latticeBasis_one

added theorem PeriodPair.latticeBasis_zero

added def PeriodPair.latticeEquivProd

added theorem PeriodPair.latticeEquiv_symm_apply

added theorem PeriodPair.lattice_eq_span_range_basis

added theorem PeriodPair.mem_lattice

added theorem PeriodPair.mul_ω₁_add_mul_ω₂_mem_lattice

added theorem PeriodPair.ω₁_div_two_notMem_lattice

added theorem PeriodPair.ω₁_mem_lattice

added theorem PeriodPair.ω₂_div_two_notMem_lattice

added theorem PeriodPair.ω₂_mem_lattice

added def PeriodPair.℘

added def PeriodPair.℘Except

added theorem PeriodPair.℘Except_add

added theorem PeriodPair.℘Except_def

added theorem PeriodPair.℘Except_neg

added theorem PeriodPair.℘Except_of_notMem

added theorem PeriodPair.℘_bound

added theorem PeriodPair.℘_neg

added structure PeriodPair

Modified Mathlib/LinearAlgebra/Basis/Basic.lean