The doc_alias command

Intended for use within Literature/ files to give paper-numbered names (e.g. theorem_2_1) the docstrings of the declarations that they alias.

def «commandDoc_alias_:=_» : Lean.ParserDescr

doc_alias new := target creates new as an alias of target, copying target's docstring: @[inherit_doc target] alias new := target.

Equations

• One or more equations did not get rendered due to their size.