Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-03-03 11:12
e518fb05
View on Github →
feat: ae strongly measurable with respect to compProd (
#22381
)
Estimated changes
Modified
Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
added
theorem
MeasureTheory.AEStronglyMeasurable.ae_of_compProd