Commit 2024-02-06 09:06 71843741

View on Github →

chore: tidy various files (#10269)

Estimated changes

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

modified theorem ContinuousLinearEquiv.integral_comp_comm

modified theorem LinearIsometry.integral_comp_comm

modified theorem MeasureTheory.set_integral_mono

modified theorem MeasureTheory.set_integral_mono_ae

modified theorem MeasureTheory.set_integral_nonpos_of_ae

modified theorem MeasureTheory.set_integral_nonpos_of_ae_restrict

modified theorem integral_conj

modified theorem integral_ofReal