Commit 2025-08-17 14:27 db35195a

View on Github →

fix(RingTheory/Ideal): quick fix Oka.lean (#28525) I just noticed a naming discrepancy between the doc and the actual name of results in Oka.lean that I missed in #27200. The deprecation may not really be necessary since the theorem was added yesterday but better be safe. This PR is also the occasion to clean a little bit the proof of IsOka.isPrime_of_maximal_not_isOka.

Estimated changes

Modified Mathlib/RingTheory/Ideal/Oka.lean

added theorem Ideal.IsOka.forall_of_forall_prime

deleted theorem Ideal.IsOka.forall_of_forall_prime_isOka

added theorem Ideal.IsOka.isPrime_of_maximal_not

deleted theorem Ideal.IsOka.isPrime_of_maximal_not_isOka