[Merged by Bors] - chore(data/mv_polynomial): Rename variables

[shingtaklam1324]

I renamed α to R throughout. I also changed the \sigma to σ in basic.lean, see leanprover-community/doc-gen#62

---

Formerly: The file used α and β as the semirings, not R and S as suggested by the original module doc string.

[jcommelin]

While I agree that this should be fixed, I would rather see that the docstring stays the same and the variables in the file get updated to "meaninful" variable names. That seems to be the tendency in mathlib.
If you don't have energy for that refactor right now, then I'm happy to merge this, because consistency is more important than progress (-;

[shingtaklam1324]

I have a week or two before term so I'm happy to fix it if you prefer all the mv_polynomial files used R as the (semi)ring. It's much easier to change α to R than the other way round ;)

The ones that use α are basic.lean, comm_ring.lean, equiv.lean, rename.lean and variables.lean. My only concern right now is that there is 5 open PRs for mv_polynomials, I don't think merge conflicts will be a big issue but I'm not sure.

[jcommelin]

Of those five files, one of my PRs fixes rename.lean. I think I don't touch comm_ring.lean at all. For the rest... we'll fix merge conflicts when we see them (-;

[shingtaklam1324]

Alright then. I won't touch rename.lean but I'll change the rest.

[shingtaklam1324]

I did a search-and-replace changing all the αs to Rs. Hopefully I didn't break anything.

Question: There are lemmas which have other (semi)rings β, γ, δ etc. Should I change β => S, γ => T, δ => U? Or should I use other letters (if S, T, U have any particular meanings?)

[jcommelin]

Yes, that looks good to me. Other common letters for (commutative) rins/algebras are A, B, C

[jcommelin]

Hmm, sorry, addition: I think I would rather use R₁ and R₂ or S₁ etc, instead of T or U... those are not so common letters for rings.

[shingtaklam1324]

Thanks. I'll change those once I figure out why the build broke.

[shingtaklam1324]

This is a bit annoying, (and I suspect a lot more has been broken). The order of the arguments has been changed in aeval by my renaming.

[jcommelin]

Right... this is exactly why we would like to have all the variables renamed, because they were used with very different meanings in different declarations.

[shingtaklam1324]

Reason for the above breakage is this change. As R was already being used as a variable in this part of the file, when I changed α to R, Lean complains that R already exists, so I deleted the R from this sections. This then changed the order of arguments for aeval

[jcommelin]

Ok... It would be good to keep the order of variables as much the same as possible. (Otherwise this refactor might ramify into many other files, which seems undesirable.)

[shingtaklam1324]

Actually the build succeeded, so there was only one breakage. I think if I rename β, γ, δ etc. then I can get rid of the A on L821 and the type arguments should be together, and the typeclass ones together. The only change would then be σ S being changed to S σ in the previous comment.

[shingtaklam1324]

Wait, the previous comment isn't right. comm_semiring R will still come before f.

The easiest way forward is just to use the original variables but with new names. Then nothing should be broken. But I'm not sure if that's the right way.

[jcommelin]

I'll let you do what you think is best (-;

[shingtaklam1324]

Alright thanks. If there's only one breakage in mathlib then I'm not too concerned about it to be perfectly honest.

[jcommelin]

Thanks 🎉

bors merge

[bors]

This PR was included in a batch that was canceled, it will be automatically retried

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests