Mathlib Changelog
Changelog
About
Github
Commit
2023-05-20 10:41
9b33e5f3
View on Github →
feat(measure_theory/function/l1_space): generalize from fields to rings (
#19052
)
Estimated changes
Modified
src/measure_theory/function/l1_space.lean
modified
theorem
measure_theory.has_finite_integral.const_mul
modified
theorem
measure_theory.has_finite_integral.mul_const
added
theorem
measure_theory.has_finite_integral.smul'
modified
theorem
measure_theory.has_finite_integral.smul
modified
theorem
measure_theory.has_finite_integral_smul_iff
added
theorem
measure_theory.integrable_const_mul_iff
added
theorem
measure_theory.integrable_mul_const_iff