Commit 2024-01-16 07:51 b4cd3132

View on Github →

feat(MeasureTheory/Function/StronglyMeasurable): pow lemmas (#9489) This also adds some missing to_additives for vadd.

Estimated changes

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Modified Mathlib/Order/Filter/Basic.lean

deleted theorem Filter.EventuallyEq.const_smul

added theorem Filter.EventuallyEq.pow_const