Commit 2025-08-12 22:55 1b235f6e

feat(RingTheory/Ideal): Oka predicates over ideals (#27200) This PR introduces the notion of Oka predicates over the ideals of a ring. We usually speak of Oka families but predicates seemed more in line with mathlib's conventions. Currently this notions isn't used anywhere but we plan to make an other PR that proves that is all prime ideals of a ring are finitely generated, then this ring is Noetherian. We can also use Oka predicates to simplify the existing proof of IsPrincipalIdealRing.of_prime.