multiplicative, additive

Stream: general

[Yaël Dillies]

docs#multiplicative.to_add, docs#multiplicative.of_add, docs#additive.to_mul, docs#additive.of_mul are a confusing set of names. All other translation operations between type synonyms use to_synonym : α → synonym α (or a decoration thereof) and of_synonym : synonym α → α, but here we have to_first_synonym : second_synonym α → α and of_first_synonym : α → second_synonym α!

[Yaël Dillies]

Would people be for renaming

• multiplicative.to_add → multiplicative.of_mul
• multiplicative.of_add → multiplicative.to_mul
• additive.to_mul → additive.of_add
• additive.of_mul → additive.to_add

[Eric Wieser]

I quite like the existing names

[Eric Wieser]

of_add should be read as "of the type where we're using +" not "of additive"

[Yaël Dillies]

I understand the current names, I'm just saying that I use more brain power than needed because they don't follow the pattern.

[Yaël Dillies]

Writing a proof yesterday, I had to go through all four to find the correct one.

[Eric Wieser]

Can you list the other synonyms you're thinking of?

[Yaël Dillies]

docs#order_dual, docs#sym_alg are the ones that come to mind immediately.

[Eric Wieser]

docs#mul_opposite, docs#add_opposite also come to mind

[Yaël Dillies]

They use a slightly different scheme, as otherwise we would have expected to_op and of_op.

[Eric Wieser]

It's worth noting that three of those four synonyms are involutive, order_dual (order_dual X) = X is morally true, whereas the titular synonyms satisfy multiplicative (additive X) = X

[Eric Wieser]

I think that partially justifies why the names are easier to confuse

[Michael Stoll]

I would hope to get rid of most cases where one presently needs to use of_add and friends by having morphisms between additive and multiplicative structures (and conversely). In any case, please don't change the names until #15684 gets merged (I need to use them there a few times).

[Yaël Dillies]

As further evidence, I just made the mistake in #15719 again :face_palm: