Theorem MeasureTheory.SimpleFunc.coe_intCast

Modification history

2026-10-21 09:51

Mathlib/MeasureTheory/Function/SimpleFunc.lean

feat: use `IsApply` for `SimpleFunc` (#45077)

Deleted MeasureTheory.SimpleFunc.coe_intCast View on Github →

2025-07-26 23:35

Mathlib/MeasureTheory/Function/SimpleFunc.lean

feat(MeasureTheory/SimpleFunc): add instances of algebraic structures (#27336) …

Added MeasureTheory.SimpleFunc.coe_intCast View on Github →