Commit 2026-05-19 17:03 d7aa7de3

View on Github →

feat(Analysis/Calculus/Deriv): add deriv_const_op (#39082) This PR adds some lemmas so simp can automatically evaluate derivatives of partially applied heterogeneous operations such as HAdd.hAdd, HSub.hSub, HMul.hMul HDiv.hDiv, and HPow.hPow.

Estimated changes

added theorem deriv_const_add_id'
added theorem deriv_const_add_id
added theorem deriv_const_sub'
modified theorem deriv_const_sub
added theorem deriv_const_sub_id'
added theorem deriv_const_sub_id
added theorem deriv_const_div
added theorem deriv_const_div_id
added theorem deriv_const_rpow_id