# Zulip Chat Archive

## Stream: new members

### Topic: to_additive and nested namespaces

#### Amelia Livingston (Dec 11 2019 at 19:55):

Hallo - sorry I can't work this out from the documentation in `to_additive.lean`

, but how do I get `localization.monoid`

to transport to `add_localization.add_monoid`

instead?

import algebra.group.to_additive variables (α : Type*) @[to_additive add_localization] def localization := α namespace localization.monoid @[to_additive] lemma foo : true := trivial end localization.monoid #check add_localization.monoid.foo -- add_localization.monoid.foo : true

I don't really want to write `@[to_additive add_localization.add_monoid.foo]`

at the beginning of everything, and `attribute [to_additive add_localization.add_monoid] localization.monoid`

doesn't make sense because `localization.monoid`

is an unknown identifier, and those are my only ideas :( Thank you in advance.

#### Yury G. Kudryashov (Dec 13 2019 at 00:34):

Indeed this is not documented. Try

run_cmd to_additive.map_namespace `localization.monoid `add_localization.add_monoid

#### Yury G. Kudryashov (Dec 13 2019 at 00:36):

Lean doesn't allow us to have attributes on namespaces, so `to_additive.map_namespace`

creates an auxiliary `def`

named `src._to_additive`

.

#### Yury G. Kudryashov (Dec 13 2019 at 00:37):

I should probably review the `to_additive`

documentation, and add it to `tactic.md`

.

#### Amelia Livingston (Dec 13 2019 at 20:28):

Thank you so much, this works great!

Last updated: May 15 2021 at 02:11 UTC