Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-22 15:16 f6d397fc

View on Github →

feat(order/hom/basic): order_iso_class (#12157) Define order_iso_class, following the hom refactor. Also add a few missing lemmas.

Estimated changes

Modified src/data/equiv/basic.lean

Modified src/linear_algebra/basic.lean

deleted theorem linear_map.map_le_map_iff

Modified src/linear_algebra/quotient.lean

Modified src/order/hom/basic.lean

added theorem order_iso.ext

added theorem order_iso.to_fun_eq_coe