Theorem Ideal.IsPrime.one_notMem

Modification history

2025-06-23 08:19
Mathlib/RingTheory/Ideal/Prime.lean
feat(RingTheory): IsPrime.one_notMem (#26203)
Added Ideal.IsPrime.one_notMemView on Github →