# Zulip Chat Archive

## Stream: new members

### Topic: Naming convention for the additive version of a lemma

#### Sebastian Monnet (Feb 10 2022 at 14:05):

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 (Feb 10 2022 at 14:49):

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

#### Eric Wieser (Feb 10 2022 at 14:50):

Ah, it's docs#left_add_coset

#### Sebastian Monnet (Feb 10 2022 at 16:11):

Thanks, I've committed it as `is_open.left_add_coset`

#### Eric Wieser (Feb 10 2022 at 16:37):

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 (Feb 10 2022 at 16:38):

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

Last updated: Dec 20 2023 at 11:08 UTC