Commit 2023-07-06 09:30 93bf611b

View on Github →

feat: define action of Mᵈᵐᵃ on α →ₘ[μ] β (#5693) See #5379

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/AEEqFun/DomAct.lean

added theorem DomMulAct.mk_smul_mk_aeeqFun

added theorem DomMulAct.smul_aeeqFun_aeeq

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

added theorem MeasureTheory.AEStronglyMeasurable.comp_measurePreserving