Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-13 17:25 ca56c5ad

View on Github →

feat(measure_theory/group): define a few measurable_equivs (#10299)

Estimated changes

Modified src/data/equiv/mul_add.lean

added theorem equiv.inv_symm₀

Created src/measure_theory/group/measurable_equiv.lean

added theorem measurable_embedding_const_smul

added theorem measurable_embedding_const_smul₀

added theorem measurable_embedding_mul_left

added theorem measurable_embedding_mul_left₀

added theorem measurable_embedding_mul_right

added theorem measurable_embedding_mul_right₀

added theorem measurable_equiv.coe_mul_left

added theorem measurable_equiv.coe_mul_left₀

added theorem measurable_equiv.coe_mul_right

added theorem measurable_equiv.coe_mul_right₀

added theorem measurable_equiv.coe_smul₀

added def measurable_equiv.inv

added def measurable_equiv.inv₀

added def measurable_equiv.mul_left

added def measurable_equiv.mul_left₀

added def measurable_equiv.mul_right

added def measurable_equiv.mul_right₀

added def measurable_equiv.smul

added def measurable_equiv.smul₀

added theorem measurable_equiv.symm_inv

added theorem measurable_equiv.symm_inv₀

added theorem measurable_equiv.symm_mul_left

added theorem measurable_equiv.symm_mul_left₀

added theorem measurable_equiv.symm_mul_right

added theorem measurable_equiv.symm_mul_right₀

added theorem measurable_equiv.symm_smul

added theorem measurable_equiv.symm_smul₀

added theorem measurable_equiv.to_equiv_mul_left

added theorem measurable_equiv.to_equiv_mul_left₀

added theorem measurable_equiv.to_equiv_mul_right

added theorem measurable_equiv.to_equiv_mul_right₀