Add lemma to root namespace without leaving a namespace

Stream: general

[Yury G. Kudryashov]

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?

[Mario Carneiro]

No

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

Then I'll go with private lemma, alias