Wikipedia · test · AMS 14
easyknown result, no worker yet
Jacobian conjecture
Exercise · jacobian_conjecture_identity
The formal statement below is all there is.
Formal statement · Lean 4.lean
theorem jacobian_conjecture_identity (H : JacobianConjectureProp k σ) :
∃ (G : RegularFunction k σ σ), G.comp (id k σ) = id k σ ∧
(id k σ).comp G = id k σ := by
sorryProof. sorry
Nobody has tried yet.