nat_clog_helper

Mathlib.Tactic.NormNum.NatLog

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.nat_clog_helper

Lean4

theorem nat_clog_helper {b m n : ℕ} (hb : Nat.blt 1 b = true) (h₁ : Nat.blt (b ^ m) n = true)
    (h₂ : Nat.ble n (b ^ (m + 1)) = true) : Nat.clog b n = m + 1 :=
  by
  rw [Nat.blt_eq] at hb
  rw [Nat.blt_eq, ← Nat.lt_clog_iff_pow_lt hb] at h₁
  rw [Nat.ble_eq, ← Nat.clog_le_iff_le_pow hb] at h₂
  cutsat

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru