Theorem Ideal.IsOka.forall_of_forall_prime'

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) …
Added Ideal.IsOka.forall_of_forall_prime'View on Github →