Structure Ideal.IsOka

Modification history

2025-08-12 22:55
Mathlib/RingTheory/Ideal/Oka.lean
feat(RingTheory/Ideal): Oka predicates over ideals (#27200) …
Added Ideal.IsOkaView on Github →