Additive aliases

Stream: general

[Yaël Dillies]

If you have a look at file#algebra/order/group around line 500, you'll see that the to_additive attribute is not automatically bestowed onto aliases created using alias. Could we make it so that an alias of a declaration marked to_additive is automatically additivized?

[Yaël Dillies]

@Joachim Breitner you might be interested in doing this.

[Yaël Dillies]

Whoever does this should be aware that the relevant existing uses of to_additive won't break because to_additive silently fails when a lemma name is already taken: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/alias.20silently.20succeeds.20when.20name.20already.20exists

[Yaël Dillies]

Joachim, this will also fix a bunch of the current to_additive_doc nolints: When bar is declared an alias of foo, it gets a docstring **Alias** of `foo`., but additivizing them both does not make add_bar have docstring **Alias** of `add_foo`..
Example: docs#inv_le_of_inv_le' vs docs#neg_le_of_neg_le

[Alex J. Best]

I think at one point I made it so that to_additive would copy the alias attribute, with the intention that if someone to_additived an alias probably the original name was to_additived too

[Alex J. Best]

What you suggest also makes sense, but thats something to keep in mind if someone ends up adding this

[Yaël Dillies]

Given that alias is something you do post declaration (although I guess that could change) while to_additive is used on the spot, it makes more sense to me that the default behavior is to_additive first, then alias.