Theorem MonomialOrder.lex_le_iff_of_unique

Modification history

2025-01-30 12:44

Mathlib/Data/Finsupp/MonomialOrder.lean

feat(Data/Finsupp/MonomialOrder) : lexicographic order on `Unique` (#20699) …

Added MonomialOrder.lex_le_iff_of_unique View on Github →