Theorem Pi.lex_desc

Modification history

2025-03-19 06:49

Mathlib/Order/PiLex.lean

feat: generalize Mathlib.Order (#23062) …

Modified Pi.lex_desc View on Github →

2023-08-18 15:36

Mathlib/Data/Pi/Lex.lean

feat: ordered monoid instances for lexicographic order on Prod, Pi, Finsupp and Dfinsupp (#6625)

Modified Pi.lex_desc View on Github →

2022-12-20 13:42

Mathlib/Data/Pi/Lex.lean

feat: port Data.Pi.Lex (#1104) …

Added Pi.lex_desc View on Github →