Theorem Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver

Modification history

2026-09-29 11:08
Mathlib/RingTheory/QuasiFinite/Basic.lean
chore: rename remaining `not_mem` declarations to `notMem` (#44296) …
Deleted Ideal.exists_not_mem_forall_mem_of_ne_of_liesOverView on Github →
2026-01-22 12:40
Mathlib/RingTheory/Etale/QuasiFinite.lean
feat(RingTheory): predicate for `QuasiFiniteAt` (#33718)
Modified Ideal.exists_not_mem_forall_mem_of_ne_of_liesOverView on Github →
2026-01-06 11:03
Mathlib/RingTheory/Etale/QuasiFinite.lean
feat(RingTheory): construct etale neighborhood that isolates point in fiber (#32823)
Added Ideal.exists_not_mem_forall_mem_of_ne_of_liesOverView on Github →