Def MeasureTheory.SimpleFunc.ofFintype

Modification history

2024-02-06 07:47

Mathlib/MeasureTheory/Function/SimpleFunc.lean

chore(MeasureTheory): `Fintype` -> `Finite` (#10289) …

Deleted MeasureTheory.SimpleFunc.ofFintype View on Github →

2023-09-15 18:54

Mathlib/MeasureTheory/Function/SimpleFunc.lean

feat: Pmf.integral_eq_sum (#6454) …

Added MeasureTheory.SimpleFunc.ofFintype View on Github →