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] to MeasureTheory.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.

Estimated changes