Theorem Ideal.IsPrime.mul_not_mem

Modification history

2025-05-25 12:30
Mathlib/RingTheory/Ideal/Prime.lean
chore(*): not_mem/nmem -> notMem (#25159)
Deleted Ideal.IsPrime.mul_not_memView on Github →
2025-04-11 13:00
Mathlib/RingTheory/Ideal/Prime.lean
feat(RingTheory/Polynomial/Eisenstein/Generalized): a generalized version of the Eisenstein criterion (#23710) …
Added Ideal.IsPrime.mul_not_memView on Github →