Commit 2025-10-22 23:09 0a7093c0
View on Github →chore(MeasureTheory/Function/SimpleFunc): deprecate SimpleFunc.coe_le (#30737)
This PR deprecates the duplicate MeasureTheory.SimpleFunc.coe_le of coe_le_coe that seems to have accidentally slipped in via #18707.