Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-04-10 06:23
08f27d03
View on Github →
feat: Bochner integral against the counting measure (
#23864
) From LeanAPAP
Estimated changes
Modified
Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
added
theorem
MeasureTheory.integral_count