advancedresearch / poi

a pragmatic point-free theorem prover assistant
Apache License 2.0
136 stars 7 forks source link

Fixed `∂((x - s)^\k) / (∂ * x!>s) => k * (x - s) ^ (k - 1);` #958

Closed bvssvni closed 3 years ago

bvssvni commented 3 years ago

The partial derivative does not treat constants as constants in the context after taking the derivative, so it must expand directly.