Commit 2024-07-15 20:56 b84e04dc
View on Github →feat(Group/Action): add smul_ae
(#14575)
- drop measurability assumption in
MeasureTheory.measure_smul_null
; - add
measure_smul_eq_zero_iff
,smul_mem_ae
, andsmul_ae
.
feat(Group/Action): add smul_ae
(#14575)
MeasureTheory.measure_smul_null
;measure_smul_eq_zero_iff
, smul_mem_ae
, and smul_ae
.