Commit 2025-12-02 17:09 e5aa51ad

View on Github →

chore(Analysis): rename ℘ to weierstrassP (#32354)

Estimated changes

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

added theorem PeriodPair.differentiableOn_weierstrassP

added theorem PeriodPair.differentiableOn_weierstrassPExcept

deleted theorem PeriodPair.differentiableOn_℘

deleted theorem PeriodPair.differentiableOn_℘Except

added theorem PeriodPair.hasSumLocallyUniformly_weierstrassP

added theorem PeriodPair.hasSumLocallyUniformly_weierstrassPExcept

deleted theorem PeriodPair.hasSumLocallyUniformly_℘

deleted theorem PeriodPair.hasSumLocallyUniformly_℘Except

added theorem PeriodPair.hasSum_weierstrassP

added theorem PeriodPair.hasSum_weierstrassPExcept

deleted theorem PeriodPair.hasSum_℘

deleted theorem PeriodPair.hasSum_℘Except

added def PeriodPair.weierstrassP

added def PeriodPair.weierstrassPExcept

added theorem PeriodPair.weierstrassPExcept_add

added theorem PeriodPair.weierstrassPExcept_def

added theorem PeriodPair.weierstrassPExcept_neg

added theorem PeriodPair.weierstrassPExcept_of_notMem

added theorem PeriodPair.weierstrassP_bound

added theorem PeriodPair.weierstrassP_neg

deleted def PeriodPair.℘

deleted def PeriodPair.℘Except

deleted theorem PeriodPair.℘Except_add

deleted theorem PeriodPair.℘Except_def

deleted theorem PeriodPair.℘Except_neg

deleted theorem PeriodPair.℘Except_of_notMem

deleted theorem PeriodPair.℘_bound

deleted theorem PeriodPair.℘_neg