Mathlib v3 is deprecated. Go to Mathlib v4

Def order.ideal.principal

Modification history

2022-04-25 04:29

src/order/ideal.lean

refactor(order/ideal): Make `order.ideal` extend `lower_set` (#13070) …

Modified order.ideal.principal View on Github →

2020-06-08 19:05

src/order/ideal.lean

feat(order/ideal): order ideals, cofinal sets and the Rasiowa-Sikorski lemma (#2850) …

Added order.ideal.principal View on Github →