Theorem Ideal.le_colon

Modification history

2026-01-16 14:47

Mathlib/RingTheory/Ideal/Colon.lean

feat(RingTheory/Ideal): generalize Submodule.colon to sets (#33390) …

Modified Ideal.le_colon View on Github →

2025-08-12 22:55

Mathlib/RingTheory/Ideal/Colon.lean

feat(RingTheory/Ideal): Oka predicates over ideals (#27200) …

Added Ideal.le_colon View on Github →