Commit 2024-06-26 09:21 bc984f06

View on Github →

feat(Measure/Stieltjes): Add instance Module ℝ≥0 StieltjesFunction (#14115)

  • Add StieltjesFunction.const and StieltjesFunction.add
  • Add lemmas const_apply and add_apply
  • Add instances AddCommMonoid StieltjesFunction and Module ℝ≥0 StieltjesFunction
  • Add lemmas measure_const, measure_add and measure_smul
  • Cleanup

Estimated changes