Commit 2023-06-26 12:34 a9665a02
View on Github →feat: add MeasureTheory.inv_smul_ae_eq_self
(#5429)
- Add
MeasureTheory.inv_smul_ae_eq_self
and its additive version. - Add
@[to_additive]
toMeasureTheory.measure_smul_null
. - Fix the order of implicit arguments and universes in
MeasureTheory.vadd_ae_eq_self_of_mem_zmultiples
to match the multiplicative version.