naming inconsistency in `localization.mk`

Stream: general

[Jujian Zhang]

I don't know if this is worth reporting, but localization.mk_mul says that a/b * c/d = ac / bd and localization.add_mk says that a/b + c/d = (ad + bc)/bd. I think maybe add_mk should be mk_add as well, or the other way around.

[Anne Baanen]

(For the lazy like me: docs#localization.mk_mul, docs#localization.add_mk)

[Anne Baanen]

I vote for add_mk and mul_mk, since the head symbol (the function in the outermost brackets) is add and mul. Or mk_add_mk and mk_mul_mk would be good options.

[Yakov Pechersky]

I like mk_add_mk, because even though the head symbol is add, we always write it infix.