Commit 2025-09-12 19:09 0f2759c4
View on Github →feat(RingTheory/Ideal/IsOka): Add a variant for Ideal.IsOka.forall_of_forall_prime (#29567)
When reviewing #28451 and #28477, @kckennylau noticed that a common pattern to create the argument hmax of Ideal.IsOka.forall_of_forall_prime.
This PR factors out this common pattern inside Ideal.IsOka.forall_of_forall_prime'.