Commit 2025-07-26 11:40 d38d2356

View on Github →

feat: mark HasFiniteIntegral with fun_prop (#27506) And use it to golf a few proofs.

Estimated changes

Modified Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

modified theorem MeasureTheory.Integrable.enorm

modified theorem MeasureTheory.Integrable.norm

modified theorem MeasureTheory.integrable_zero_measure