Commit 2023-08-17 22:17 adb6afd8

View on Github →

chore(MeasureTheory): golf (#6641)

  • Golf some proofs.
  • Rename MeasureTheory.indicatorConst_empty to MeasureTheory.indicatorConstLp_empty.
  • Change some linebreaks.

Estimated changes