Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-10 08:56 c8926223

View on Github →

move(order/synonym): Group order_dual and lex (#13769) Move to_dual, of_dual, to_lex, of_lex to a new file order.synonym. This does not change the import tree, because order.lexicographic had slightly higher imports than order.order_dual, but those weren't used for lex itself.

Estimated changes

deleted def lex
deleted def of_lex
deleted theorem of_lex_inj
deleted theorem of_lex_symm_eq
deleted theorem of_lex_to_lex
deleted def to_lex
deleted theorem to_lex_inj
deleted theorem to_lex_of_lex
deleted theorem to_lex_symm_eq
added def lex
added def of_lex
added theorem of_lex_inj
added theorem of_lex_symm_eq
added theorem of_lex_to_lex
added theorem order_dual.le_to_dual
added theorem order_dual.lt_to_dual
added theorem order_dual.of_dual_inj
added theorem order_dual.to_dual_inj
added theorem order_dual.to_dual_le
added theorem order_dual.to_dual_lt
added def to_lex
added theorem to_lex_inj
added theorem to_lex_of_lex
added theorem to_lex_symm_eq