English
The matrix of the differential in the aeval-predicated sense equals the map of the Jacobian matrix by aeval(P.val).
Русский
Матрица дифференциала по отношению к aeval совпадает с отображением матрицы Якобиана через aeval(P.val).
LaTeX
$$toMatrix' P.aevalDifferential = (aeval P.val).mapMatrix P.jacobiMatrix$$
Lean4
theorem aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix :
P.aevalDifferential.toMatrix' = (aeval P.val).mapMatrix P.jacobiMatrix :=
by
ext i j : 1
rw [← LinearMap.toMatrix_eq_toMatrix']
rw [LinearMap.toMatrix_apply]
simp [jacobiMatrix_apply]
