## 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*)

namespace localization.monoid

@[to_additive] lemma foo : true := trivial

end localization.monoid



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