Theorem MeasureTheory.hasFiniteIntegral_of_fintype

Modification history

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