jacobiMatrix_apply — Mathlib

English

If σ is finite and decidable, the Jacobian can be represented as a matrix with entries d_{i j} = ∂(P.map i)/∂(P.relation j).

Русский

Если σ конечен и имеетсяDecidableEq, Якобиан задаётся матрицей с элементами d_{i j} = ∂(P.map i)/∂(P.relation j).

LaTeX

$$jacobiMatrix : Matrix σ σ P.Ring with (P.jacobiMatrix)_{i j} = ∂(P.map i)/∂(P.relation j)$$

Lean4

theorem jacobiMatrix_apply (i j : σ) : P.jacobiMatrix i j = MvPolynomial.pderiv (P.map i) (P.relation j) := by
  simp [jacobiMatrix, LinearMap.toMatrix, differential, basis]

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