Documentation

Mathlib.Tactic.NormNum.NatLog

norm_num extensions for Nat.log and Nat.clog #

This module defines norm_num extensions for Nat.log and Nat.clog.

source
def Mathlib.Meta.NormNum.proveNatLog (eb en : Q(ℕ)) :
(ek : Q(ℕ)) × Q(Nat.log «$eb» «$en» = «$ek»)

Given the natural number literals eb and en, returns Nat.log eb en as a natural number literal and an equality proof. Panics if ex or en aren't natural number literals.

Equations
    Instances For
      source
      def Mathlib.Meta.NormNum.evalNatLog :
      NormNumExt

      Evaluates the Nat.log function.

      Equations
        Instances For
          source
          theorem Mathlib.Meta.NormNum.nat_clog_helper {b m n : ℕ} (hb : Nat.blt 1 b = true) (h₁ : (b ^ m).blt n = true) (h₂ : n.ble (b ^ (m + 1)) = true) :
          Nat.clog b n = m + 1
          source
          def Mathlib.Meta.NormNum.proveNatClog (eb en : Q(ℕ)) :
          (ek : Q(ℕ)) × Q(Nat.clog «$eb» «$en» = «$ek»)

          Given the natural number literals eb and en, returns Nat.clog eb en as a natural number literal and an equality proof. Panics if ex or en aren't natural number literals.

          Equations
            Instances For
              source
              def Mathlib.Meta.NormNum.evalNatClog :
              NormNumExt

              Evaluates the Nat.clog function.

              Equations
                Instances For