Commit 2024-07-31 19:18 cdcd8836

View on Github →

chore(SimpleFunc): use FunLike (#6642)

Estimated changes

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

modified theorem MeasureTheory.SimpleFunc.coe_injective

added theorem MeasureTheory.SimpleFunc.coe_mk

modified theorem MeasureTheory.SimpleFunc.ext

Modified Mathlib/MeasureTheory/Integral/Bochner.lean