Theorem Ideal.IsOka.isPrime_of_maximal_not

Modification history

2025-09-12 19:09
Mathlib/RingTheory/Ideal/Oka.lean
feat(RingTheory/Ideal/IsOka): Add a variant for `Ideal.IsOka.forall_of_forall_prime` (#29567) …
Modified Ideal.IsOka.isPrime_of_maximal_notView on Github →
2025-08-17 14:27
Mathlib/RingTheory/Ideal/Oka.lean
fix(RingTheory/Ideal): quick fix Oka.lean (#28525) …
Added Ideal.IsOka.isPrime_of_maximal_notView on Github →