Mathlib Changelog
v4
Changelog
About
Github
Theorem
Real.rpowIntegrand₀₁_zero_right
Modification history
2025-05-08 00:39
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean
feat(SpecialFunctions): Integral representation of `rpow` over `Ioo 0 1` (#24393) …
Added
Real.rpowIntegrand₀₁_zero_right
View on Github →