## Stream: general

### Topic: Add lemma to root namespace without leaving a namespace

#### Yury G. Kudryashov (Feb 20 2020 at 07:07):

How can I add a lemma to the root namespace without leaving the namespace block? I understand that I can define a lemma, then use alias command. Is there any more straightforward way?

No

#### Mario Carneiro (Feb 20 2020 at 07:12):

More generally, any tactic can create a declaration with any name, but you can't use the def or theorem keyword to create a new lemma outside the namespace

#### Mario Carneiro (Feb 20 2020 at 07:14):

I guess with some user command magic you can make something that acts passably close to theorem

#### Mario Carneiro (Feb 20 2020 at 07:14):

but there are lots of little things that are hard to replicate, like pulling in variables from the section

#### Yury G. Kudryashov (Feb 20 2020 at 08:01):

Then I'll go with private lemma, alias

Last updated: May 08 2021 at 20:11 UTC