Theorem Ideal.mem_jacobson_bot

Modification history

2026-10-28 11:47
Mathlib/RingTheory/Jacobson/Ideal.lean
chore(RingTheory/Jacobson): use `Ring.jacobson` throughout the library (#44788) …
Modified Ideal.mem_jacobson_botView on Github →
2023-05-18 05:52
Mathlib/RingTheory/JacobsonIdeal.lean
feat port RingTheory.JacobsonIdeal (#4061)
Added Ideal.mem_jacobson_botView on Github →