Commit 2025-04-02 09:26 ab457a50

View on Github →

feat: a few lemmas from the Carleson project (#23545)

Estimated changes

Modified Mathlib/Analysis/RCLike/Basic.lean

added theorem RCLike.enorm_conj

Modified Mathlib/Data/ENNReal/Inv.lean

Modified Mathlib/Data/NNReal/Defs.lean

added theorem Real.toNNReal_zpow

Modified Mathlib/Topology/Algebra/Support.lean

added theorem ContinuousOn.continuous_of_mulTSupport_subset