Documentation

Mathlib.Tactic.Lemma

Support for lemma as a synonym for theorem. #

source
def lemma :
Lean.ParserDescr

lemma means the same as theorem. It is used to denote "less important" theorems

Equations
    Instances For
      source
      def expandLemma :
      Lean.Macro

      Implementation of the lemma command, by macro expansion to theorem.

      Equations
        Instances For