isUnit_jacobian_of_linearIndependent_of_span_eq_top

English

Under the stated hypotheses, the Jacobian is a unit, as proven by standard linear-algebra criteria.

Русский

При заданных предположениях Якобиан является единицей, что следует из стандартных критериев линейной алгебры.

LaTeX

$$IsUnit(P.jacobian)$$

Lean4

theorem isUnit_jacobian_of_linearIndependent_of_span_eq_top
    (hli : LinearIndependent S (fun j i : σ ↦ aeval P.val <| pderiv (P.map i) (P.relation j)))
    (hsp : Submodule.span S (Set.range <| (fun j i : σ ↦ aeval P.val <| pderiv (P.map i) (P.relation j))) = ⊤) :
    IsUnit P.jacobian := by
  classical
  rw [isUnit_jacobian_iff_aevalDifferential_bijective]
  exact
    LinearMap.bijective_of_linearIndependent_of_span_eq_top (Pi.basisFun _ _).span_eq (by convert hli; simp)
      (by convert hsp; simp)

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