Theorem IsArtinianRing.exists_not_mem_forall_mem_of_ne

Modification history

2026-09-29 11:08
Mathlib/RingTheory/Spectrum/Prime/Noetherian.lean
chore: rename remaining `not_mem` declarations to `notMem` (#44296) …
Deleted IsArtinianRing.exists_not_mem_forall_mem_of_neView on Github →
2026-04-28 15:42
Mathlib/RingTheory/Spectrum/Prime/Noetherian.lean
feat(RingTheory/Spectrum/Prime/Noetherian): rank of an Artinian ring over a field (#38182) …
Modified IsArtinianRing.exists_not_mem_forall_mem_of_neView on Github →
2026-01-06 11:03
Mathlib/RingTheory/Spectrum/Prime/Noetherian.lean
feat(RingTheory): construct etale neighborhood that isolates point in fiber (#32823)
Added IsArtinianRing.exists_not_mem_forall_mem_of_neView on Github →