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) …

Modified Ideal.IsOka.forall_of_forall_prime View on Github →

2025-08-17 14:27

Mathlib/RingTheory/Ideal/Oka.lean

fix(RingTheory/Ideal): quick fix Oka.lean (#28525) …

Added Ideal.IsOka.forall_of_forall_prime View on Github →