Jacobian matrix

Jacobiandef

The Jacobian matrix of a RegularFunction: the matrix of formal partial derivatives ∂Fⱼ/∂xᵢ. Note that its entries are polynomials, not scalars — it is a matrix that varies from point to point.

noncomputable def RegularFunction.Jacobian {k : Type*} [CommRing k] {σ τ : Type*}
    (F : RegularFunction k σ τ) : Matrix σ τ (MvPolynomial σ k) :=
  Matrix.of fun i j => MvPolynomial.pderiv i (F j)

Builds on

Regular function

Used by

Keller map

From Mathlib

Algebra.MvPolynomial.PDeriv
LinearAlgebra.Matrix.Determinant.Basic

import Conjectura.Defs.Mathematics.AlgebraicGeometry.Jacobian · maintainer — open · raw source

Adapted for Conjectura from formal-conjectures (Google DeepMind), `FormalConjectures/Wikipedia/JacobianConjecture.lean`. Split into one concept per module; no mathematical content changed.

Copyright (c) 2025 The Formal Conjectures Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Formal Conjectures Authors

Full credits