clog_zpow

Mathlib.Data.Int.Log

URI: https://scilib.ai/kg/mathlib#Int.clog_zpow

English

For base b > 1 and any integer z, clog_b(b^z) = z.

Русский

Для основания b>1 и любого целого z выполняется clog_b(b^z) = z.

LaTeX

$$$\operatorname{clog}_b(b^{z})=z, \quad b>1, z\in\mathbb{Z}$$$

Lean4

theorem clog_zpow {b : ℕ} (hb : 1 < b) (z : ℤ) : clog b (b ^ z : R) = z := by
  rw [← neg_log_inv_eq_clog, ← zpow_neg, log_zpow hb, neg_neg]

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

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

Разделы

Аффилиация

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