neg_log_inv_eq_clog

Mathlib.Data.Int.Log

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

English

The negative of the logarithm of an inverse equals clog: −log_b(r^{-1}) = clog_b(r).

Русский

Отрицательный логарифм обратного равен clog: −log_b(r^{-1}) = clog_b(r).

LaTeX

$$$-\log_b(r^{-1}) = \operatorname{clog}(b,r)$$$

Lean4

theorem neg_log_inv_eq_clog (b : ℕ) (r : R) : -log b r⁻¹ = clog b r := by rw [log_inv, neg_neg]

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

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

Разделы

Аффилиация

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