Mathlib v3 is deprecated. Go to Mathlib v4

Theorem max_rec

Modification history

2022-07-11 16:51
src/order/basic.lean
fix(order/basic): fix `subtype.linear_order` (#15056) …
Modified max_recView on Github →
2021-10-04 15:09
src/algebra/order/functions.lean
feat(algebra/order/functions): recursors and images under monotone maps (#9505)
Added max_recView on Github →