Wikipedia · textbook · AMS 13 16

mediumknown result, no worker yet

Jacobson Conjecture

Theorem · jacobson_conjecture_of_comm_ring

For commutative rings this is the case as a consequence of Krull's intersection theorem.

Formal statement · Lean 4.lean
theorem jacobson_conjecture_of_comm_ring (R : Type u) [CommRing R] [IsNoetherianRing R] :
    JacobsonConjectureFor R := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗