Mathlib v3 is deprecated. Go to Mathlib v4

Theorem order_iso.to_fun_eq_coe

Modification history

2022-02-22 15:16
src/order/hom/basic.lean
feat(order/hom/basic): `order_iso_class` (#12157) …
Added order_iso.to_fun_eq_coeView on Github →