neg_clog_inv_eq_log

Mathlib.Data.Int.Log

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

English

The negative of clog(b, r^{-1}) equals log(b, r); equivalently, -clog_b(r^{-1}) = log_b(r).

Русский

Отрицательное значение clog(b, r^{-1}) равно log_b(r): -clog_b(r^{-1}) = log_b(r).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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