Commit 2025-03-10 12:57 d8860297

View on Github →

chore: review of porting notes in MeasureTheory/ (#22671)

Estimated changes

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

deleted theorem MeasureTheory.det_one_smulRight

Modified Mathlib/MeasureTheory/Function/L2Space.lean

Modified Mathlib/MeasureTheory/Group/Integral.lean

Modified Mathlib/MeasureTheory/Group/LIntegral.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

Modified Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

Modified Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

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

added theorem MeasureTheory.isAddHaarMeasure_volume_pi

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/Topology/Algebra/Module/Determinant.lean

added theorem ContinuousLinearMap.det_one_smulRight