renaming incorrect names?

Stream: mathlib4

[Thomas Murrills]

I found an incorrectly named identifier in mathlib4; is the general policy to leave those as-is (at least for now), or should I PR? It's relatively minor, so I just wanted to check if it's worth it right now. (the identifier is mkpair, which should be mkPair)

[Eric Wieser]

Fixing mis-ported names is definitely a good thing to do

[Eric Wieser]

Fixing mis-ported names is definitely a good thing to go

[Thomas Murrills]

!4#2324 :)