Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_disjoint_smul_of_is_compact

Modification history

2022-11-17 16:08
src/topology/algebra/group.lean
feat(measure_theory/integral): integral composed with smul (#17455)
Added exists_disjoint_smul_of_is_compactView on Github →