Commit 2026-01-13 15:36 d803dd35

View on Github →

feat(Analytic): ℘'(z)² = 4 ℘(z)³ - g₂ ℘(z) - g₃ (#33723)

Estimated changes

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

added theorem IsZLattice.isCompact_range_of_periodic

Modified Mathlib/Analysis/Analytic/Order.lean

added theorem analyticOrderAt_id

added theorem natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Operations.lean

modified theorem ContDiff.smul

modified theorem ContDiffAt.smul

modified theorem ContDiffOn.smul

modified theorem ContDiffWithinAt.smul

modified theorem contDiff_smul

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean

added theorem Filter.EventuallyEq.iteratedDerivWithin_eq

added theorem Filter.EventuallyEq.iteratedDerivWithin_eq_of_nhds_insert

added theorem iteratedDerivWithin_fun_id

added theorem iteratedDerivWithin_id

added theorem iteratedDerivWithin_mul

added theorem iteratedDerivWithin_pow

added theorem iteratedDerivWithin_smul

added theorem iteratedDeriv_fun_add

added theorem iteratedDeriv_fun_id

added theorem iteratedDeriv_fun_id_zero

added theorem iteratedDeriv_fun_mul

added theorem iteratedDeriv_fun_pow_zero

added theorem iteratedDeriv_fun_sub

added theorem iteratedDeriv_id

added theorem iteratedDeriv_mul

added theorem iteratedDeriv_pow

Modified Mathlib/Analysis/Meromorphic/Basic.lean

added theorem Meromorphic.const

Modified Mathlib/Analysis/Meromorphic/Order.lean

added theorem AnalyticAt.of_meromorphicOrderAt_pos

added theorem meromorphicOrderAt_id

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

added def PeriodPair.G

added theorem PeriodPair.G_eq_zero_of_odd

deleted theorem PeriodPair.PeriodPairs.analyticOnNhd_derivWeierstrassP

added theorem PeriodPair.analyticAt_derivWeierstrassPExcept

added theorem PeriodPair.analyticAt_weierstrassPExcept

added theorem PeriodPair.analyticOnNhd_derivWeierstrassP

added theorem PeriodPair.compl_lattice_diff_singleton_mem_nhds

added theorem PeriodPair.derivWeierstrassPExcept_zero_zero

added theorem PeriodPair.derivWeierstrassP_sq

added theorem PeriodPair.deriv_derivWeierstrassPExcept_self

added theorem PeriodPair.deriv_weierstrassPExcept_same

added def PeriodPair.g₂

added def PeriodPair.g₃

added theorem PeriodPair.hasFPowerSeriesAt_derivWeierstrassPExcept

added theorem PeriodPair.hasFPowerSeriesAt_weierstrassPExcept

added theorem PeriodPair.iteratedDeriv_derivWeierstrassPExcept_self

added theorem PeriodPair.iteratedDeriv_weierstrassPExcept_self

added theorem PeriodPair.meromorphic_derivWeierstrassP

added theorem PeriodPair.sumInvPow_zero

added theorem PeriodPair.weierstrassPExcept_zero

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

Modified Mathlib/Geometry/Manifold/Instances/Sphere.lean