Theorem DFinsupp.colex_lt_iff_of_unique

Modification history

2025-12-02 05:38
Mathlib/Data/DFinsupp/Lex.lean
feat: colex order on (dependent) finsupps (#30482)
Added DFinsupp.colex_lt_iff_of_uniqueView on Github →