Mathlib v3 is deprecated. Go to Mathlib v4

Def linear_order.lift'

Modification history

2022-07-11 16:51
src/order/basic.lean
fix(order/basic): fix `subtype.linear_order` (#15056) …
Added linear_order.lift'View on Github →