# `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

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

Instances For

source
def Mathlib.Meta.NormNum.evalNatLog :
NormNumExt

Evaluates the `Nat.log` function.

Equations

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

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

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

Instances For

source
def Mathlib.Meta.NormNum.evalNatClog :
NormNumExt

Evaluates the `Nat.clog` function.

Equations

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

Instances For