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, and smul_ae.

Estimated changes

added theorem MeasureTheory.smul_ae