isUnit_jacobian_iff_aevalDifferential_bijective

English

Same logical content as previous, stated in alternate form.

Русский

Та же идея в другой формулировке: единичность Якобиана эквивалентна биективности производного.

LaTeX

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

Lean4

theorem isUnit_jacobian_iff_aevalDifferential_bijective : IsUnit P.jacobian ↔ Function.Bijective P.aevalDifferential :=
  by
  rw [P.jacobian_eq_det_aevalDifferential, ← LinearMap.isUnit_iff_isUnit_det]
  exact Module.End.isUnit_iff P.aevalDifferential

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