Commit 2025-04-14 20:38 2d000560
View on Github →chore(Data/Finsupp/MonomialOrder/DegLex): dedup instance (#24046) Split from #23976 The remaining instance is at https://github.com/leanprover-community/mathlib4/blob/03e9f15f2acafae1d9d3b7e0674ba87ae3cd499c/Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean#L125-L129