Leading Term of Multivariate Polynomial

Stream: new members

[AHan]

I wanted to write a function which return the leading term of a multivariate polynomial
But I have no idea how to do it with the multivariate polynomial in mathlib ....

[Mario Carneiro]

what is the leading term of a multivariate polynomial?

[Mario Carneiro]

like y^2 + x*y + x^2 + y

[AHan]

For example:
leading term of (XY + X + Y) is XY

[AHan]

leading term of y^2 + x*y + x^2 + y will depends on our choice

[AHan]

So have to define a monomial ordering first
i.e If u ≤ v and w is any other monomial, then u w ≤ v w