Theorem Finsupp.Lex.single_strictAnti

Modification history

2025-10-28 10:18

Mathlib/Data/Finsupp/Lex.lean

feat: `CoeFun` for `Lex` and `Colex` (#30481) …

Modified Finsupp.Lex.single_strictAnti View on Github →

2024-12-04 18:37

Mathlib/Data/Finsupp/Lex.lean

feat(Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order (#19455) …

Added Finsupp.Lex.single_strictAnti View on Github →