Finsupp.degree

Stream: mathlib4

[Violeta Hernández]

Out of curiosity, why is docs#Finsupp.degree called that? I would have expected that name to be used for f.support.max or something similar.

[Damiano Testa]

I think that this function is intended to be the finsupp of exponents of a monomial. So the degree is the sum of the entries.

[Violeta Hernández]

Oh, it's the degree of a monomial, not a polynomial

[Violeta Hernández]

Fair enough.

[Jovan Gerbscheid]

Shouldn't it be called Finsupp.sum?

[Ruben Van de Velde]

That's something else

[Jovan Gerbscheid]

Hmm, that's true

[Damiano Testa]

Maybe to help the intuition, the Finsupp should be called MonomialExponents or something like this. :upside_down:

[Junyan Xu]

Finsupp.total has been deprecated for more than 6 months, so the name is available now :) Feels like resale of expired domain name, should we make it an auction? :explode:

[Jovan Gerbscheid]

It seems that this has already been suggested in the past ^^
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Finsupp.2Etotal/near/465989771