Mathlib v3 is deprecated. Go to Mathlib v4

Theorem of_lex_inj

Modification history

2022-05-10 08:56
src/order/lexicographic.lean
move(order/synonym): Group `order_dual` and `lex` (#13769) …
Modified of_lex_injView on Github →
2022-01-03 20:30
src/order/lexicographic.lean
refactor(order/lexicographic): Change the `lex` synonym (#10926) …
Added of_lex_injView on Github →