Theorem Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver

Modification history

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_liesOver View 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_liesOver View on Github →