Commit 2023-05-11 05:53 5ed65e18

View on Github →

feat: port MeasureTheory.Group.MeasurableEquiv (#3912)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Group/MeasurableEquiv.lean

added theorem MeasurableEquiv.coe_mulLeft

added theorem MeasurableEquiv.coe_mulLeft₀

added theorem MeasurableEquiv.coe_mulRight

added theorem MeasurableEquiv.coe_mulRight₀

added theorem MeasurableEquiv.coe_smul₀

added def MeasurableEquiv.divLeft

added def MeasurableEquiv.divRight

added def MeasurableEquiv.inv

added def MeasurableEquiv.mulLeft

added def MeasurableEquiv.mulLeft₀

added def MeasurableEquiv.mulRight

added def MeasurableEquiv.mulRight₀

added def MeasurableEquiv.smul

added def MeasurableEquiv.smul₀

added theorem MeasurableEquiv.symm_inv

added theorem MeasurableEquiv.symm_mulLeft

added theorem MeasurableEquiv.symm_mulLeft₀

added theorem MeasurableEquiv.symm_mulRight

added theorem MeasurableEquiv.symm_mulRight₀

added theorem MeasurableEquiv.symm_smul

added theorem MeasurableEquiv.symm_smul₀

added theorem MeasurableEquiv.toEquiv_mulLeft

added theorem MeasurableEquiv.toEquiv_mulLeft₀

added theorem MeasurableEquiv.toEquiv_mulRight

added theorem MeasurableEquiv.toEquiv_mulRight₀

added theorem measurableEmbedding_const_smul

added theorem measurableEmbedding_const_smul₀

added theorem measurableEmbedding_mulLeft

added theorem measurableEmbedding_mulLeft₀

added theorem measurableEmbedding_mulRight

added theorem measurableEmbedding_mulRight₀