Commit 2024-01-08 11:01 494478bf

View on Github →

chore: Rename rpow_nonneg_of_nonneg to rpow_nonneg (#9518) This better matches other lemma names. From LeanAPAP

Estimated changes

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/Fourier/PoissonSummation.lean

Modified Mathlib/Analysis/MeanInequalities.lean

Modified Mathlib/Analysis/MeanInequalitiesPow.lean

Modified Mathlib/Analysis/MellinTransform.lean

Modified Mathlib/Analysis/NormedSpace/PiLp.lean

Modified Mathlib/Analysis/NormedSpace/ProdLp.lean

Modified Mathlib/Analysis/NormedSpace/lpSpace.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian.lean

Modified Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals.lean

Modified Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

added theorem Real.rpow_nonneg

deleted theorem Real.rpow_nonneg_of_nonneg

Modified Mathlib/Analysis/SpecificLimits/FloorPow.lean

Modified Mathlib/Combinatorics/Additive/Behrend.lean

Modified Mathlib/Computability/AkraBazzi/AkraBazzi.lean

Modified Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm.lean

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean

Modified Mathlib/NumberTheory/Bertrand.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

Modified Mathlib/NumberTheory/NumberField/Discriminant.lean

Modified Mathlib/NumberTheory/ZetaFunction.lean