Automating Mathematics

Working journal

A subtle differentiable function is the scalar product,

for a vector space $V$.

Derivative

By Liebniz rule, the total derivative is

Note that depends on the vector space structure on $(\mathbb{R}, V)$. For a vector $w$ in $V$, note that we can write

Code

We need an additional implicit structure with combinators: