When computing determinants that depend on a parameter $t\in \Bbb R$, it is often useful to use the fact that \begin{align} \det(V_1(t),\dots,V_n(t))&=\det(V_1(a),\dots,V_n(a))+\\ &\int_a^t\left(\det (V_1'(t),\dots,V_n(t))+\dots+\det(V_1(t),\dots,V_n'(t))\right)\,dt \end{align} I was wondering if this could lead to results that wouldn't be valid in another field $\Bbb K\not = \Bbb R$ where $V_1(t),\dots,V_n(t)$ and the final result can be given a similar meaning for $t\in \Bbb K$ (even though some steps of the proof could have no meaning in $\Bbb K$).
On the one hand, you will always be able to compute the determinant and I can't see why the you wouldn't be able to prove that those two expressions that should be equal are. But on the other hand, I can't see how you can algorithmically transform a proof using derivatives into a proof that doesn't use it...
I'm pretty sure that since you can define the derivative of a polynomial in an algebraic way, if $V_1,\dots,V_n$ are polynomials, you'll probably be able to use the proof with derivatives even though you wouldn't justify each step the same way.
I'm hoping for
Either a proof that no matter how you find your formula for the determinant for $t\in \Bbb R$, as long as the first and last formula make sense for $t\in\Bbb K$, the formula will be true
Or a counterexample.
My intuition tells me there should be some way to "divide by zero" in the proof by taking $\Bbb K$ with a finite characteristic to find a counterexample but I didn't find it...
Given a field $\mathbb K$, we can consider the ring of polynomials $\mathbb K[t]$ in one unknown $t$. We have formal derivatives $D\colon \mathbb K[t]\to\mathbb K[t]$, given by $Dt^n=nt^{n-1}$. However, in general we lack formal integration. For $f=\sum_{k\ge 0} a_k t^k$, we would wish to define $I(f)=\; "\!\!\int_0^tf\,\mathrm dt\!"\;=\sum_{k\ge 1}\frac{a_{k-1}}kt^k$. But that may fail because division by $k\in\mathbb N$ may not be defined in nonzero characteristics.
But: Your original formula can in fact be shown with formal derivatives and integrationin $\mathbb Z[a_{11},\ldots,a_{nn},t]$, and then the result is readily transferred to an arbitrary base ring.