clog_natCast — Mathlib

English

For natural b and n with n ≥ 2, clog(b, n) equals Nat.clog(b, n) viewed in the ambient field.

Русский

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

LaTeX

$$$\operatorname{clog}(b, n) = \mathrm{Nat.clog}(b, n) \;\;\text{(cast to } \mathbb{R})$$$

Lean4

@[simp, norm_cast]
theorem clog_natCast (b : ℕ) (n : ℕ) : clog b (n : R) = Nat.clog b n :=
  by
  rcases n with - | n
  · simp [clog_of_right_le_one]
  · rw [clog_of_one_le_right, (Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr] <;> simp

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