Mathlib Changelog
v4
Changelog
About
Github
Theorem
MeasureTheory.integrable_of_fintype
Modification history
2024-02-06 07:47
Mathlib/MeasureTheory/Function/L1Space.lean
chore(MeasureTheory): `Fintype` -> `Finite` (#10289) …
Deleted
MeasureTheory.integrable_of_fintype
View on Github →
2023-09-15 18:54
Mathlib/MeasureTheory/Function/L1Space.lean
feat: Pmf.integral_eq_sum (#6454) …
Added
MeasureTheory.integrable_of_fintype
View on Github →