lemma — Mathlib

Lean4
/-- `lemma` means the same as `theorem`. It is used to denote "less important" theorems -/
@[command_parser 1001]
public meta def lemma : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `lemma 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `declModifiers)
      (ParserDescr.unary✝ `group
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "lemma ") (ParserDescr.const✝ `declId))
            (ParserDescr.unary✝ `ppIndent (ParserDescr.const✝ `declSig)))
          (ParserDescr.const✝ `declVal))))
Похожие утверждения