Commit 2023-08-18 15:36 ffc1e0b2

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Order/Group/Prod.lean

Modified Mathlib/Algebra/Order/Monoid/Prod.lean

Modified Mathlib/Data/DFinsupp/Lex.lean

Modified Mathlib/Data/Fin/Tuple/BubbleSortInduction.lean

Modified Mathlib/Data/Finsupp/Lex.lean

Modified Mathlib/Data/Pi/Lex.lean

modified theorem Pi.lex_desc