Commit 2022-11-18 03:49 63095f3a

View on Github →

feat: port Order.Synonym (#562) mathlib3 hash: fd47bdf09e90f553519c712378e651975fe8c829

depends on: #556
depends on: #550

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Synonym.lean

added def Lex

added theorem OrderDual.le_toDual

added theorem OrderDual.lt_toDual

added def OrderDual.ofDual

added theorem OrderDual.ofDual_inj

added theorem OrderDual.ofDual_le_ofDual

added theorem OrderDual.ofDual_lt_ofDual

added theorem OrderDual.ofDual_symm_eq

added theorem OrderDual.ofDual_toDual

added def OrderDual.toDual

added theorem OrderDual.toDual_inj

added theorem OrderDual.toDual_le

added theorem OrderDual.toDual_le_toDual

added theorem OrderDual.toDual_lt

added theorem OrderDual.toDual_lt_toDual

added theorem OrderDual.toDual_ofDual

added theorem OrderDual.toDual_symm_eq

added def ofLex

added theorem ofLex_inj

added theorem ofLex_toLex

added theorem of_lex_symm_eq

added def toLex

added theorem toLex_inj

added theorem toLex_ofLex

added theorem toLex_symm_eq