Commit 2026-10-28 11:47 54f780dc

chore(RingTheory/Jacobson): use Ring.jacobson throughout the library (#44788) Existing statements about the Jacobson radical of a ring use both (⊥ : Ideal R).jacobson and Ring.jacobson R. This PR standardizes these statements on Ring.jacobson R and updates the downstream proofs, completing the TODO next to the definition of Ring.jacobson. Part of this work was originally included in #41066. The remaining changes were implemented by GPT-6.1 Sol and reviewed by me.