Commit 2025-06-23 08:19 ee285be6

View on Github →

feat(RingTheory): IsPrime.one_notMem (#26203)

Estimated changes

Modified Mathlib/RingTheory/Ideal/Prime.lean

added theorem Ideal.IsPrime.one_notMem

added theorem Ideal.one_notMem