Commit 2025-05-13 18:29 e9db98be

feat(Data/Finsupp/MonomialOrder): give ≼[m]/ ≺[m] the same priority as ≤/< (#24832) a ≼[m] b ∨ b ≼[m] a would be parsed as (a ≼[m] b) ∨ (b ≼[m] a). The previous priority of the left and right side of ≼[m] and ≺[m] is lower than logic connectives, which makes statements like a ≼[m] b ∨ b ≼[m] a parsed as a ≼[m] (b ∨ b) ≼[m] a, and statements like (a ≼[m] b) ∨ b ≼[m] a parsed as ((a ≼[m] b) ∨ b) ≼[m] a. With this commit, both of them would be parsed as (a ≼[m] b) ∨ (b ≼[m] a).