Theorem Finsupp.Lex.single_antitone

Modification history

2026-05-17 20:27
Mathlib/Data/Finsupp/Lex.lean
chore: remove declarations deprecated between 2021-05-15 and 2025-11-15 (#39405) …
Deleted Finsupp.Lex.single_antitoneView on Github →
2025-10-28 10:18
Mathlib/Data/Finsupp/Lex.lean
feat: `CoeFun` for `Lex` and `Colex` (#30481) …
Modified Finsupp.Lex.single_antitoneView 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_antitoneView on Github →