Commit 2026-10-21 12:46 e83c9eaa

View on Github →

feat: use IsApply for FiniteMeasure (#45123)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

deleted theorem MeasureTheory.FiniteMeasure.coeFn_add

deleted theorem MeasureTheory.FiniteMeasure.coeFn_smul

deleted theorem MeasureTheory.FiniteMeasure.coeFn_zero

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean