Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measurable_embedding_const_smul

Modification history

2021-11-13 17:25

src/measure_theory/group/measurable_equiv.lean

feat(measure_theory/group): define a few `measurable_equiv`s (#10299)

Added measurable_embedding_const_smul View on Github →