clog_ofNat — Mathlib

English

For b and n natural with n ≥ 2, clog(b, ofNat(n)) equals Nat.clog(b, n) cast to the ambient field.

Русский

Для b и n натуральных значений (n ≥ 2) clog(b, ofNat(n)) равно Nat.clog(b, n), приведённому к полю.

LaTeX

$$$\operatorname{clog}(b, \text{ofNat}(n)) = \mathrm{Nat.clog}(b, n)$$$

Lean4

@[simp]
theorem clog_ofNat (b : ℕ) (n : ℕ) [n.AtLeastTwo] : clog b (ofNat(n) : R) = Nat.clog b ofNat(n) :=
  clog_natCast b n

Похожие утверждения