jacobiMatrix_naive — Mathlib

English

Reindexing commutes with the evaluation map: the reindexed jacobiMatrix equals the evaluation of the renamed matrix.

Русский

Перебиндирование совместимо с отображением на значения: перерассчитанный jacobiMatrix равен проверке переименованной матрицы через отображение.

LaTeX

$$$\\operatorname{jacobiMatrix}(P^{e,f}) = (\\operatorname{jacobiMatrix}(P))^{f^{-1},f^{-1}} \\mapsto \\mathrm{rename}(e^{-1})$ (formal equality shown in the theorem).$$

Lean4

@[simp]
theorem jacobiMatrix_naive [Fintype ι] [DecidableEq ι] (i j : ι) :
    (naive a ha s hs).jacobiMatrix i j = (v j).pderiv (a i) :=
  jacobiMatrix_apply _ _ _

Похожие утверждения