logb_ne_zero_of_pos_of_ne_one

Mathlib.Analysis.SpecialFunctions.Log.Base

URI: https://scilib.ai/kg/mathlib#Real.logb_ne_zero_of_pos_of_ne_one

English

Let b > 1 and x > 0 with x ≠ 1. Then log_b(x) ≠ 0.

Русский

Пусть b > 1 и x > 0, x ≠ 1. Тогда log_b(x) ≠ 0.

LaTeX

$$$b>1,\ x>0,\ x\\neq 1 \Rightarrow \log_b x \\neq 0$$$

Lean4

theorem logb_ne_zero_of_pos_of_ne_one (hx_pos : 0 < x) (hx : x ≠ 1) : logb b x ≠ 0 :=
  mt (eq_one_of_pos_of_logb_eq_zero hb hx_pos) hx

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

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

Разделы

Аффилиация

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