Commit 2025-08-27 10:43 47a36205

View on Github →

chore: remove parentheses in interval integral notation (#29017) This is possible since https://github.com/leanprover/lean4/pull/8784

Estimated changes

Modified Archive/Wiedijk100Theorems/BuffonsNeedle.lean

Modified Mathlib/Analysis/Complex/CauchyIntegral.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/Real/Pi/Wallis.lean

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

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

Modified Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean

modified theorem integral_log_from_zero

modified theorem integral_log_from_zero_of_pos

modified theorem integral_sin_pow_antitone

modified theorem integral_sin_pow_pos

modified theorem integral_sin_pow_succ_le

Modified Mathlib/Analysis/SpecialFunctions/Integrals/LogTrigonometric.lean

modified theorem integral_log_sin_zero_pi

modified theorem integral_log_sin_zero_pi_div_two

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

Modified Mathlib/MeasureTheory/Integral/CircleAverage.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

Modified Mathlib/MeasureTheory/Integral/CircleTransform.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean

modified theorem Function.Periodic.tendsto_atBot_intervalIntegral_of_pos

modified theorem Function.Periodic.tendsto_atTop_intervalIntegral_of_pos

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/NumberTheory/Harmonic/Bounds.lean

Modified Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean

Modified Mathlib/NumberTheory/ZetaValues.lean

Modified Mathlib/Probability/Distributions/Exponential.lean

Modified Mathlib/Probability/StrongLaw.lean