jacobiMatrix — Mathlib

English

The Jacobian is a unit in S if and only if the differential aeval is bijective.

Русский

Число единичности Якобиана эквивалентно биективности отображения дифференциала.

LaTeX

$$IsUnit(P.jacobian) ↔ Bijective(P.aevalDifferential)$$

Lean4

/-- If `σ` has a `Fintype` and `DecidableEq` instance, the differential of `P`
can be expressed in matrix form.
-/
noncomputable def jacobiMatrix : Matrix σ σ P.Ring :=
  LinearMap.toMatrix P.basis P.basis P.differential

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