Theorem toLex_inj

Modification history

2026-03-12 18:27

Mathlib/Order/Lex.lean

chore(Order/OrderDual): move material on `OrderDual` (#35150) …

Modified toLex_inj View on Github →

2025-03-13 11:07

Mathlib/Order/Synonym.lean

chore: review of porting notes in `Order/` (#22895)

Modified toLex_inj View on Github →

2022-11-18 03:49

Mathlib/Order/Synonym.lean

feat: port Order.Synonym (#562) …

Added toLex_inj View on Github →