Commit 2024-02-13 09:59 4f8cced6

View on Github →

feat: add Integrable.of_integral_ne_zero (#10430)

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

added theorem MeasureTheory.Integrable.of_integral_ne_zero

modified theorem MeasureTheory.integrable_of_integral_eq_one