Commit 2024-04-10 06:01 56499517

View on Github →

chore: rename five lemmas involving mathlib3 names (#11934)

Estimated changes

Modified Mathlib/Algebra/Lie/Weights/Linear.lean

added theorem LieModule.trace_comp_toEndomorphism_weightSpace_eq

deleted theorem LieModule.trace_comp_toEndomorphism_weight_space_eq

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

added theorem MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded

added theorem MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded_left

added theorem MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded_right

deleted theorem MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded

deleted theorem MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded_left

deleted theorem MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded_right

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

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

added theorem EuclideanSpace.volume_ball

added theorem EuclideanSpace.volume_closedBall

deleted theorem Euclidean_space.volume_ball

deleted theorem Euclidean_space.volume_closedBall