Theorem MeasureTheory.average_eq'

Modification history

2023-06-11 13:19

Mathlib/MeasureTheory/Integral/Average.lean

chore: copy integral notation precedence from mathport (#4963) …

Modified MeasureTheory.average_eq'View on Github →

2023-06-06 04:28

Mathlib/MeasureTheory/Integral/Average.lean

feat: port MeasureTheory.Integral.Average (#4709)

Added MeasureTheory.average_eq'View on Github →