Theorem Ideal.IsOka.isPrime_of_maximal_not_isOka

Modification history

2025-08-17 14:27
Mathlib/RingTheory/Ideal/Oka.lean
fix(RingTheory/Ideal): quick fix Oka.lean (#28525) …
Deleted Ideal.IsOka.isPrime_of_maximal_not_isOkaView on Github →
2025-08-12 22:55
Mathlib/RingTheory/Ideal/Oka.lean
feat(RingTheory/Ideal): Oka predicates over ideals (#27200) …
Added Ideal.IsOka.isPrime_of_maximal_not_isOkaView on Github →