Naming convention for the additive version of a lemma

Stream: new members

[Sebastian Monnet]

I'm working on a PR (#11876), proving

import topology.algebra.group

variables (G : Type*) [topological_space G] [group G] [has_continuous_mul G]

lemma is_open.left_coset {U : set G} (x : G) (h : is_open U) :
is_open (left_coset x U) :=
is_open_map_mul_left x _ h

and the corresponding lemmas for open/closed left/right cosets. @Oliver Nash pointed out that the additive versions should also be included, which I think I should do with

import topology.algebra.group

variables (G : Type*) [topological_space G] [group G] [has_continuous_mul G]

@[to_additive is_open.add_left_coset]
lemma is_open.left_coset {U : set G} (x : G) (h : is_open U) :
is_open (left_coset x U) :=
is_open_map_mul_left x _ h

Here I've named the additive version is_open.add_left_coset, but I'm not sure if this is the right convention. What should this lemma be called?

[Eric Wieser]

That would be consistent with docs#add_left_coset, if that exists

[Eric Wieser]

Ah, it's docs#left_add_coset

[Sebastian Monnet]

Thanks, I've committed it as is_open.left_add_coset

[Eric Wieser]

It looks like you might have missed the main point of @Oliver Nash's comment on Zulip, which was:

For some reason to_additive doesn't know to transport left_coset to left_add_coset.

I suggest asking for help about this on Zulip.

I think Oliver's point is that ideally to_additive would be able to generate the name automatically, rather than you having to provide it.

[Eric Wieser]

Fixing that is probably out of scope for the PR, but might be worth doing in a follow-up PR