Theorem MeasureTheory.SimpleFunc.coe_mk

Modification history

2024-07-31 19:18
Mathlib/MeasureTheory/Function/SimpleFunc.lean
chore(SimpleFunc): use `FunLike` (#6642)
Added MeasureTheory.SimpleFunc.coe_mkView on Github →