Mathlib v3 is deprecated. Go to Mathlib v4

Theorem order.ideal.coe_sup

Modification history

2022-04-25 04:29

src/order/ideal.lean

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

Added order.ideal.coe_sup View on Github →