Implicit/explicit arguments in similar situations in Mathlib

Stream: new members

[Philippe Duchon]

While playing around with polynomials and power series in Mathlib, both in the single and multiple variable cases, I noticed that the monomial function has the ring of coefficients implicit for polynomials, but explicit for power series.

import Mathlib

#check MvPolynomial.monomial
-- implicit R
#check MvPowerSeries.monomial
-- explicit R

I suppose there is a good reason for this, but I am having a hard time figuring out what it can be.

(I have not checked the libary files for a similar difference between the two, this is just the first case where I noticed the difference)

[Ruben Van de Velde]

Could also be an accident

[Riccardo Brasca]

It is most likely an accident. Not 100% clear which one is better. If you want you can try to make R implicit and see if you have to add a lot of (R := R).