Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-31 18:58 66f7114a

View on Github →

feat(measure_theory/group): add measurable_set.const_smul (#10025) Partially based on lemmas from #2819.

Estimated changes

Modified src/algebra/pointwise.lean

added theorem subsingleton_zero_smul_set

added theorem zero_smul_subset

Created src/measure_theory/group/pointwise.lean

added theorem measurable_set.const_smul

added theorem measurable_set.const_smul_of_ne_zero

added theorem measurable_set.const_smul₀

Modified src/measure_theory/measurable_space_def.lean

added theorem set.subsingleton.measurable_set